𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
⊢ ∀ (x : C(X, 𝕜)), x ∈ Subalgebra.topologicalClosure A
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
⊢ Subalgebra.topologicalClosure A = ⊤
rw [Algebra.eq_top_iff]
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
⊢ ∀ (x : C(X, 𝕜)), x ∈ Subalgebra.topologicalClosure A
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
⊢ ∀ (x : C(X, 𝕜)), x ∈ Subalgebra.topologicalClosure A
let I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ofRealClm.compLeftContinuous ℝ X
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
⊢ ∀ (x : C(X, 𝕜)), x ∈ Subalgebra.topologicalClosure A
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
⊢ ∀ (x : C(X, 𝕜)), x ∈ Subalgebra.topologicalClosure A
have key : LinearMap.range I ≤ (A.toSubmodule.restrictScalars ℝ).topologicalClosure := by
  let A₀ : Submodule ℝ C(X, ℝ) := (A.toSubmodule.restrictScalars ℝ).comap I
  have SW : A₀.topologicalClosure = ⊤ :=
    haveI :=
      subalgebra_topologicalClosure_eq_top_of_separatesPoints _ (hA.isROrC_to_real hA')
    congr_arg Subalgebra.toSubmodule this
  rw [← Submodule.map_top, ← SW]
  have h₁ := A₀.topologicalClosure_map ((@ofRealClm 𝕜 _).compLeftContinuousCompact X)
  have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I
  exact h₁.trans (Submodule.topologicalClosure_mono h₂)
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
⊢ f ∈ Subalgebra.topologicalClosure A
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
⊢ ∀ (x : C(X, 𝕜)), x ∈ Subalgebra.topologicalClosure A
intro f
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
⊢ f ∈ Subalgebra.topologicalClosure A
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
⊢ f ∈ Subalgebra.topologicalClosure A
let f_re : C(X, ℝ) := (⟨IsROrC.re, IsROrC.reClm.continuous⟩ : C(𝕜, ℝ)).comp f
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
⊢ f ∈ Subalgebra.topologicalClosure A
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
⊢ f ∈ Subalgebra.topologicalClosure A
let f_im : C(X, ℝ) := (⟨IsROrC.im, IsROrC.imClm.continuous⟩ : C(𝕜, ℝ)).comp f
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
⊢ f ∈ Subalgebra.topologicalClosure A
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
⊢ f ∈ Subalgebra.topologicalClosure A
have h_f_re : I f_re ∈ A.topologicalClosure := key ⟨f_re, rfl⟩
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
h_f_im : ↑I f_im ∈ Subalgebra.topologicalClosure A
⊢ f ∈ Subalgebra.topologicalClosure A
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
⊢ f ∈ Subalgebra.topologicalClosure A
have h_f_im : I f_im ∈ A.topologicalClosure := key ⟨f_im, rfl⟩
case h.e'_4
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
h_f_im : ↑I f_im ∈ Subalgebra.topologicalClosure A
⊢ f = ↑I f_re + IsROrC.I • ↑I f_im
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
h_f_im : ↑I f_im ∈ Subalgebra.topologicalClosure A
⊢ f ∈ Subalgebra.topologicalClosure A
convert A.topologicalClosure.add_mem h_f_re (A.topologicalClosure.smul_mem h_f_im IsROrC.I)
case h.e'_4.h
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
h_f_im : ↑I f_im ∈ Subalgebra.topologicalClosure A
a✝ : X
⊢ ↑f a✝ = ↑(↑I f_re + IsROrC.I • ↑I f_im) a✝
case h.e'_4
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
h_f_im : ↑I f_im ∈ Subalgebra.topologicalClosure A
⊢ f = ↑I f_re + IsROrC.I • ↑I f_im
ext
case h.e'_4.h.h
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
h_f_im : ↑I f_im ∈ Subalgebra.topologicalClosure A
a✝ : X
⊢ ↑(↑I f_re + IsROrC.I • ↑I f_im) a✝ = ↑f a✝
case h.e'_4.h
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
h_f_im : ↑I f_im ∈ Subalgebra.topologicalClosure A
a✝ : X
⊢ ↑f a✝ = ↑(↑I f_re + IsROrC.I • ↑I f_im) a✝
apply Eq.symm
no goals
case h.e'_4.h.h
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
key : LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp (mk ↑re) f
f_im : C(X, ℝ) := comp (mk ↑im) f
h_f_re : ↑I f_re ∈ Subalgebra.topologicalClosure A
h_f_im : ↑I f_im ∈ Subalgebra.topologicalClosure A
a✝ : X
⊢ ↑(↑I f_re + IsROrC.I • ↑I f_im) a✝ = ↑f a✝
simp [mul_comm IsROrC.I _]
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
⊢ LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
⊢ LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
let A₀ : Submodule ℝ C(X, ℝ) := (A.toSubmodule.restrictScalars ℝ).comap I
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
SW : Submodule.topologicalClosure A₀ = ⊤
⊢ LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
⊢ LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
have SW : A₀.topologicalClosure = ⊤ :=
  haveI :=
    subalgebra_topologicalClosure_eq_top_of_separatesPoints _ (hA.isROrC_to_real hA')
  congr_arg Subalgebra.toSubmodule this
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
SW : Submodule.topologicalClosure A₀ = ⊤
⊢ Submodule.map I (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
SW : Submodule.topologicalClosure A₀ = ⊤
⊢ LinearMap.range I ≤ Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
rw [← Submodule.map_top, ← SW]
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
SW : Submodule.topologicalClosure A₀ = ⊤
h₁ :
  Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealClm)) (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealClm)) A₀)
⊢ Submodule.map I (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
SW : Submodule.topologicalClosure A₀ = ⊤
⊢ Submodule.map I (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
have h₁ := A₀.topologicalClosure_map ((@ofRealClm 𝕜 _).compLeftContinuousCompact X)
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
SW : Submodule.topologicalClosure A₀ = ⊤
h₁ :
  Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealClm)) (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealClm)) A₀)
h₂ :
  Submodule.map I (Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))) ≤
    Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A)
⊢ Submodule.map I (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
SW : Submodule.topologicalClosure A₀ = ⊤
h₁ :
  Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealClm)) (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealClm)) A₀)
⊢ Submodule.map I (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I
no goals
𝕜 : Type u_1
X : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra 𝕜 C(X, 𝕜)
hA : Subalgebra.SeparatesPoints A
hA' : ConjInvariantSubalgebra (Subalgebra.restrictScalars ℝ A)
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealClm
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
SW : Submodule.topologicalClosure A₀ = ⊤
h₁ :
  Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealClm)) (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealClm)) A₀)
h₂ :
  Submodule.map I (Submodule.comap I (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))) ≤
    Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A)
⊢ Submodule.map I (Submodule.topologicalClosure A₀) ≤
    Submodule.topologicalClosure (Submodule.restrictScalars ℝ (↑Subalgebra.toSubmodule A))
exact h₁.trans (Submodule.topologicalClosure_mono h₂)