[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : (fun φ => ↑↑φ) φ = (fun φ => ↑↑φ) ψ
⊢ φ = ψ
[PROOFSTEP]
ext1
[GOAL]
case a
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : (fun φ => ↑↑φ) φ = (fun φ => ↑↑φ) ψ
⊢ ↑φ = ↑ψ
[PROOFSTEP]
apply FunLike.ext
[GOAL]
case a.h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : (fun φ => ↑↑φ) φ = (fun φ => ↑↑φ) ψ
⊢ ∀ (x : A), ↑↑φ x = ↑↑ψ x
[PROOFSTEP]
exact congr_fun h
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : TopologicalSpace A
inst✝¹ : Module 𝕜 A
inst✝ : Subsingleton A
φ : ↑(characterSpace 𝕜 A)
x : A
⊢ ↑↑φ x = ↑0 x
[PROOFSTEP]
rw [show x = 0 from Subsingleton.elim x 0, map_zero, map_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
⊢ characterSpace 𝕜 A ∪ {0} ≤ {φ | ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
rintro φ (hφ | rfl)
[GOAL]
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ φ ∈ {φ | ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
exact hφ.2
[GOAL]
case inr
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
⊢ 0 ∈ {φ | ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
exact fun _ _ => by exact (zero_mul (0 : 𝕜)).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
x✝¹ x✝ : A
⊢ ↑0 (x✝¹ * x✝) = ↑0 x✝¹ * ↑0 x✝
[PROOFSTEP]
exact (zero_mul (0 : 𝕜)).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : ContinuousAdd 𝕜
inst✝⁵ : ContinuousConstSMul 𝕜 𝕜
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : TopologicalSpace A
inst✝² : Module 𝕜 A
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A ∪ {0})
[PROOFSTEP]
simp only [union_zero, Set.setOf_forall]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : ContinuousAdd 𝕜
inst✝⁵ : ContinuousConstSMul 𝕜 𝕜
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : TopologicalSpace A
inst✝² : Module 𝕜 A
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (⋂ (i : A) (i_1 : A), {x | ↑x (i * i_1) = ↑x i * ↑x i_1})
[PROOFSTEP]
exact
  isClosed_iInter fun x =>
    isClosed_iInter fun y => isClosed_eq (eval_continuous _) <| (eval_continuous _).mul (eval_continuous _)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
⊢ ↑φ 1 = 1
[PROOFSTEP]
have h₁ : φ 1 * (1 - φ 1) = 0 := by rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
⊢ ↑φ 1 * (1 - ↑φ 1) = 0
[PROOFSTEP]
rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
⊢ ↑φ 1 = 1
[PROOFSTEP]
rcases mul_eq_zero.mp h₁ with (h₂ | h₂)
[GOAL]
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : ↑φ 1 = 0
⊢ ↑φ 1 = 1
[PROOFSTEP]
have : ∀ a, φ (a * 1) = 0 := fun a => by simp only [map_mul φ, h₂, mul_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : ↑φ 1 = 0
a : A
⊢ ↑φ (a * 1) = 0
[PROOFSTEP]
simp only [map_mul φ, h₂, mul_zero]
[GOAL]
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : ↑φ 1 = 0
this : ∀ (a : A), ↑φ (a * 1) = 0
⊢ ↑φ 1 = 1
[PROOFSTEP]
exact False.elim (φ.prop.1 <| ContinuousLinearMap.ext <| by simpa only [mul_one] using this)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : ↑φ 1 = 0
this : ∀ (a : A), ↑φ (a * 1) = 0
⊢ ∀ (x : A), ↑↑φ x = ↑0 x
[PROOFSTEP]
simpa only [mul_one] using this
[GOAL]
case inr
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : 1 - ↑φ 1 = 0
⊢ ↑φ 1 = 1
[PROOFSTEP]
exact (sub_eq_zero.mp h₂).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
map_one' : ∀ (φ : ↑(characterSpace 𝕜 A)), ↑φ 1 = 1
src✝ : NonUnitalAlgHomClass (↑(characterSpace 𝕜 A)) 𝕜 A 𝕜 := instNonUnitalAlgHomClass
φ : ↑(characterSpace 𝕜 A)
r : 𝕜
⊢ ↑φ (↑(algebraMap 𝕜 A) r) = ↑(algebraMap 𝕜 𝕜) r
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, Algebra.id.map_eq_id, RingHom.id_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
map_one' : ∀ (φ : ↑(characterSpace 𝕜 A)), ↑φ 1 = 1
src✝ : NonUnitalAlgHomClass (↑(characterSpace 𝕜 A)) 𝕜 A 𝕜 := instNonUnitalAlgHomClass
φ : ↑(characterSpace 𝕜 A)
r : 𝕜
⊢ ↑φ (r • 1) = r
[PROOFSTEP]
rw [map_smul, Algebra.id.smul_eq_mul, map_one' φ, mul_one]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
⊢ characterSpace 𝕜 A = {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
ext φ
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ characterSpace 𝕜 A ↔ φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case h.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ characterSpace 𝕜 A → φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
rintro hφ
[GOAL]
case h.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
lift φ to characterSpace 𝕜 A using hφ
[GOAL]
case h.refine'_1.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : { x // x ∈ characterSpace 𝕜 A }
⊢ ↑φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
exact ⟨map_one φ, map_mul φ⟩
[GOAL]
case h.refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y} → φ ∈ characterSpace 𝕜 A
[PROOFSTEP]
rintro ⟨hφ₁, hφ₂⟩
[GOAL]
case h.refine'_2.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ₁ : ↑φ 1 = 1
hφ₂ : ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y
⊢ φ ∈ characterSpace 𝕜 A
[PROOFSTEP]
refine' ⟨_, hφ₂⟩
[GOAL]
case h.refine'_2.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ₁ : ↑φ 1 = 1
hφ₂ : ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y
⊢ φ ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case h.refine'_2.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
hφ₁ : ↑0 1 = 1
hφ₂ : ∀ (x y : A), ↑0 (x * y) = ↑0 x * ↑0 y
⊢ False
[PROOFSTEP]
exact zero_ne_one hφ₁
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A)
[PROOFSTEP]
rw [eq_set_map_one_map_mul, Set.setOf_and]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed ({a | ↑a 1 = 1} ∩ {a | ∀ (x y : A), ↑a (x * y) = ↑a x * ↑a y})
[PROOFSTEP]
refine' IsClosed.inter (isClosed_eq (eval_continuous _) continuous_const) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed {a | ∀ (x y : A), ↑a (x * y) = ↑a x * ↑a y}
[PROOFSTEP]
simpa only [(union_zero 𝕜 A).symm] using union_zero_isClosed _ _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
⊢ φ = ψ
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
have : x - algebraMap 𝕜 A (ψ x) ∈ RingHom.ker φ := by
  simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ x - ↑(algebraMap 𝕜 A) (↑ψ x) ∈ RingHom.ker φ
[PROOFSTEP]
simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
this : x - ↑(algebraMap 𝕜 A) (↑ψ x) ∈ RingHom.ker φ
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this 
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : Ring A
inst✝¹ : TopologicalSpace A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
z : 𝕜
⊢ ↑φ (↑(algebraMap 𝕜 A) z) = z
[PROOFSTEP]
simp only [AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
⊢ (fun a => mk fun φ => ↑φ a) 1 = 1
[PROOFSTEP]
ext a
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a : ↑(characterSpace 𝕜 A)
⊢ ↑((fun a => mk fun φ => ↑φ a) 1) a = ↑1 a
[PROOFSTEP]
simp only [coe_mk, coe_one, Pi.one_apply, map_one a]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
      OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } b
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
a✝ : ↑(characterSpace 𝕜 A)
⊢ ↑(OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } (a * b))
      a✝ =
    ↑(OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
          OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } b)
      a✝
[PROOFSTEP]
simp only [map_mul, coe_mk, coe_mul, Pi.mul_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : A),
                OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                    (a * b) =
                  OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
                    OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } b) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a✝ : ↑(characterSpace 𝕜 A)
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : A),
                    OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                        (a * b) =
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          a *
                        OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          b) })
          0)
      a✝ =
    ↑0 a✝
[PROOFSTEP]
simp only [map_zero, coe_mk, coe_mul, coe_zero, Pi.zero_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : A),
                OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                    (a * b) =
                  OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
                    OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } b) })
      (a + b) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : A),
                  OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                      (a * b) =
                    OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
                      OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                        b) })
        a +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : A),
                  OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                      (a * b) =
                    OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
                      OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                        b) })
        b
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
a✝ : ↑(characterSpace 𝕜 A)
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : A),
                    OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                        (a * b) =
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          a *
                        OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          b) })
          (a + b))
      a✝ =
    ↑(OneHom.toFun
            (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            a *
                          OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            b) })
            a +
          OneHom.toFun
            (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            a *
                          OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            b) })
            b)
      a✝
[PROOFSTEP]
simp only [map_add, coe_mk, coe_add, Pi.add_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
k : 𝕜
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            a *
                          OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            b) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (a b : A),
                              OneHom.toFun
                                  { toFun := fun a => mk fun φ => ↑φ a,
                                    map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                  (a * b) =
                                OneHom.toFun
                                    { toFun := fun a => mk fun φ => ↑φ a,
                                      map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                    a *
                                  OneHom.toFun
                                    { toFun := fun a => mk fun φ => ↑φ a,
                                      map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                    b) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (a b : A),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a b : A),
                                OneHom.toFun
                                    { toFun := fun a => mk fun φ => ↑φ a,
                                      map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                    (a * b) =
                                  OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      a *
                                    OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      b) })
                      (a + b) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun a => mk fun φ => ↑φ a,
                                map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : A),
                                  OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        a *
                                      OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        b) })
                        a +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun a => mk fun φ => ↑φ a,
                                map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : A),
                                  OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        a *
                                      OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        b) })
                        b) })
      (↑(algebraMap 𝕜 A) k) =
    ↑(algebraMap 𝕜 C(↑(characterSpace 𝕜 A), 𝕜)) k
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
k : 𝕜
a✝ : ↑(characterSpace 𝕜 A)
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  {
                    toOneHom :=
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a b : A),
                          OneHom.toFun
                              { toFun := fun a => mk fun φ => ↑φ a,
                                map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                              (a * b) =
                            OneHom.toFun
                                { toFun := fun a => mk fun φ => ↑φ a,
                                  map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                a *
                              OneHom.toFun
                                { toFun := fun a => mk fun φ => ↑φ a,
                                  map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                b) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun a => mk fun φ => ↑φ a,
                                map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : A),
                                  OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        a *
                                      OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        b) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun a => mk fun φ => ↑φ a,
                                  map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (a b : A),
                                    OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        (a * b) =
                                      OneHom.toFun
                                          { toFun := fun a => mk fun φ => ↑φ a,
                                            map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                          a *
                                        OneHom.toFun
                                          { toFun := fun a => mk fun φ => ↑φ a,
                                            map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                          b) })
                          (a + b) =
                        OneHom.toFun
                            (↑{
                                toOneHom :=
                                  { toFun := fun a => mk fun φ => ↑φ a,
                                    map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (a b : A),
                                      OneHom.toFun
                                          { toFun := fun a => mk fun φ => ↑φ a,
                                            map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                          (a * b) =
                                        OneHom.toFun
                                            { toFun := fun a => mk fun φ => ↑φ a,
                                              map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                            a *
                                          OneHom.toFun
                                            { toFun := fun a => mk fun φ => ↑φ a,
                                              map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                            b) })
                            a +
                          OneHom.toFun
                            (↑{
                                toOneHom :=
                                  { toFun := fun a => mk fun φ => ↑φ a,
                                    map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (a b : A),
                                      OneHom.toFun
                                          { toFun := fun a => mk fun φ => ↑φ a,
                                            map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                          (a * b) =
                                        OneHom.toFun
                                            { toFun := fun a => mk fun φ => ↑φ a,
                                              map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                            a *
                                          OneHom.toFun
                                            { toFun := fun a => mk fun φ => ↑φ a,
                                              map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                            b) })
                            b) })
          (↑(algebraMap 𝕜 A) k))
      a✝ =
    ↑(↑(algebraMap 𝕜 C(↑(characterSpace 𝕜 A), 𝕜)) k) a✝
[PROOFSTEP]
simp [AlgHomClass.commutes]
