Results on bounded continuous functions with RCLike values

theorem RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [PseudoEMetricSpace E] {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} : Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ) (Subalgebra.comap (BoundedContinuousFunction.AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)) = Subalgebra.comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).toSubalgebra)

On a star subalgebra of bounded continuous functions, the operations "restrict scalars to ℝ" and "forget that a bounded continuous function is a bounded" commute.