[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : a ∈ I
⊢ ↑(toCharacterSpace I) a = 0
[PROOFSTEP]
unfold Ideal.toCharacterSpace
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : a ∈ I
⊢ ↑(↑CharacterSpace.equivAlgHom.symm
          (AlgHom.comp (↑(AlgEquiv.symm (NormedRing.algEquivComplexOfComplete (_ : ∀ {a : A ⧸ I}, IsUnit a ↔ a ≠ 0))))
            (Quotient.mkₐ ℂ I)))
      a =
    0
[PROOFSTEP]
simp only [CharacterSpace.equivAlgHom_symm_coe, AlgHom.coe_comp, AlgHom.coe_coe, Quotient.mkₐ_eq_mk,
  Function.comp_apply, NormedRing.algEquivComplexOfComplete_symm_apply]
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : a ∈ I
⊢ Set.Nonempty.some (_ : Set.Nonempty (spectrum ℂ (↑(Quotient.mk I) a))) = 0
[PROOFSTEP]
simp_rw [Quotient.eq_zero_iff_mem.mpr ha, spectrum.zero_eq]
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : a ∈ I
⊢ Set.Nonempty.some (_ : Set.Nonempty {0}) = 0
[PROOFSTEP]
exact Set.eq_of_mem_singleton (Set.singleton_nonempty (0 : ℂ)).some_mem
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : ¬IsUnit a
⊢ ∃ f, ↑f a = 0
[PROOFSTEP]
obtain ⟨M, hM, haM⟩ := (span { a }).exists_le_maximal (span_singleton_ne_top ha)
[GOAL]
case intro.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : ¬IsUnit a
M : Ideal A
hM : IsMaximal M
haM : span {a} ≤ M
⊢ ∃ f, ↑f a = 0
[PROOFSTEP]
exact ⟨M.toCharacterSpace, M.toCharacterSpace_apply_eq_zero_of_mem (haM (mem_span_singleton.mpr ⟨1, (mul_one a).symm⟩))⟩
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
⊢ z ∈ spectrum ℂ a ↔ ∃ f, ↑f a = z
[PROOFSTEP]
refine' ⟨fun hz => _, _⟩
[GOAL]
case refine'_1
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ f, ↑f a = z
[PROOFSTEP]
obtain ⟨f, hf⟩ := WeakDual.CharacterSpace.exists_apply_eq_zero hz
[GOAL]
case refine'_1.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ ((fun x => A) z))
hf : ↑f (↑(algebraMap ℂ A) z - a) = 0
⊢ ∃ f, ↑f a = z
[PROOFSTEP]
simp only [map_sub, sub_eq_zero, AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply] at hf 
[GOAL]
case refine'_1.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ ((fun x => A) z))
hf : ↑f (↑(algebraMap ℂ A) z) = ↑f a
⊢ ∃ f, ↑f a = z
[PROOFSTEP]
refine ⟨f, ?_⟩
[GOAL]
case refine'_1.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ ((fun x => A) z))
hf : ↑f (↑(algebraMap ℂ A) z) = ↑f a
⊢ ↑f a = z
[PROOFSTEP]
rw [AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply] at hf 
[GOAL]
case refine'_1.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ ((fun x => A) z))
hf : z = ↑f a
⊢ ↑f a = z
[PROOFSTEP]
exact hf.symm
[GOAL]
case refine'_2
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
⊢ (∃ f, ↑f a = z) → z ∈ spectrum ℂ a
[PROOFSTEP]
rintro ⟨f, rfl⟩
[GOAL]
case refine'_2.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
f : ↑(characterSpace ℂ A)
⊢ ↑f a ∈ spectrum ℂ a
[PROOFSTEP]
exact AlgHom.apply_mem_spectrum f a
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
⊢ spectrum ℂ (↑(gelfandTransform ℂ A) a) = spectrum ℂ a
[PROOFSTEP]
ext z
[GOAL]
case h
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
⊢ z ∈ spectrum ℂ (↑(gelfandTransform ℂ A) a) ↔ z ∈ spectrum ℂ a
[PROOFSTEP]
rw [ContinuousMap.spectrum_eq_range, WeakDual.CharacterSpace.mem_spectrum_iff_exists]
[GOAL]
case h
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
⊢ z ∈ Set.range ↑(↑(gelfandTransform ℂ A) a) ↔ ∃ f, ↑f a = z
[PROOFSTEP]
exact Iff.rfl
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
⊢ Isometry ↑(gelfandTransform ℂ A)
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
⊢ Isometry ↑(gelfandTransform ℂ A)
[PROOFSTEP]
refine'
  AddMonoidHomClass.isometry_of_norm (gelfandTransform ℂ A) fun a =>
    _
      /- By `spectrum.gelfandTransform_eq`, the spectra of `star a * a` and its
          `gelfandTransform` coincide. Therefore, so do their spectral radii, and since they are
          self-adjoint, so also do their norms. Applying the C⋆-property of the norm and taking square
          roots shows that the norm is preserved. -/
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
⊢ ‖↑(gelfandTransform ℂ A) a‖ = ‖a‖
[PROOFSTEP]
have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by unfold spectralRadius;
  rw [spectrum.gelfandTransform_eq]
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
⊢ spectralRadius ℂ (↑(gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)
[PROOFSTEP]
unfold spectralRadius
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
⊢ ⨆ (k : ℂ) (_ : k ∈ spectrum ℂ (↑(gelfandTransform ℂ A) (star a * a))), ↑‖k‖₊ =
    ⨆ (k : ℂ) (_ : k ∈ spectrum ℂ (star a * a)), ↑‖k‖₊
[PROOFSTEP]
rw [spectrum.gelfandTransform_eq]
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
this : spectralRadius ℂ (↑(gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)
⊢ ‖↑(gelfandTransform ℂ A) a‖ = ‖a‖
[PROOFSTEP]
rw [map_mul, (IsSelfAdjoint.star_mul_self _).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
  (IsSelfAdjoint.star_mul_self (gelfandTransform ℂ A a)).spectralRadius_eq_nnnorm] at this 
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
this : ↑‖star (↑(gelfandTransform ℂ A) a) * ↑(gelfandTransform ℂ A) a‖₊ = ↑‖star a * a‖₊
⊢ ‖↑(gelfandTransform ℂ A) a‖ = ‖a‖
[PROOFSTEP]
simp only [ENNReal.coe_eq_coe, CstarRing.nnnorm_star_mul_self, ← sq] at this 
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
this : ‖↑(gelfandTransform ℂ A) a‖₊ ^ 2 = ‖a‖₊ ^ 2
⊢ ‖↑(gelfandTransform ℂ A) a‖ = ‖a‖
[PROOFSTEP]
simpa only [Function.comp_apply, NNReal.sqrt_sq] using congr_arg (((↑) : ℝ≥0 → ℝ) ∘ ⇑NNReal.sqrt) this
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
⊢ Function.Bijective ↑(gelfandTransform ℂ A)
[PROOFSTEP]
refine'
  ⟨(gelfandTransform_isometry A).injective, _⟩
    /- The range of `gelfandTransform ℂ A` is actually a `StarSubalgebra`. The key lemma below may be
        hard to spot; it's `map_star` coming from `WeakDual.Complex.instStarHomClass`, which is a
        nontrivial result. -/
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
⊢ Function.Surjective ↑(gelfandTransform ℂ A)
[PROOFSTEP]
let rng : StarSubalgebra ℂ C(characterSpace ℂ A, ℂ) :=
  { toSubalgebra := (gelfandTransform ℂ A).range
    star_mem' := by
      rintro - ⟨a, rfl⟩
      use star a
      ext1 φ
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, gelfandTransform_apply_apply, map_star, IsROrC.star_def,
        ContinuousMap.star_apply] }
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
⊢ ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
    a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
rintro - ⟨a, rfl⟩
[GOAL]
case intro
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
⊢ star (↑↑(gelfandTransform ℂ A) a) ∈
    (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
use star a
[GOAL]
case h
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
⊢ ↑↑(gelfandTransform ℂ A) (star a) = star (↑↑(gelfandTransform ℂ A) a)
[PROOFSTEP]
ext1 φ
[GOAL]
case h.h
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
φ : ↑(characterSpace ℂ A)
⊢ ↑(↑↑(gelfandTransform ℂ A) (star a)) φ = ↑(star (↑↑(gelfandTransform ℂ A) a)) φ
[PROOFSTEP]
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, gelfandTransform_apply_apply, map_star, IsROrC.star_def,
  ContinuousMap.star_apply]
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
⊢ Function.Surjective ↑(gelfandTransform ℂ A)
[PROOFSTEP]
suffices rng = ⊤ from fun x => show x ∈ rng from this.symm ▸ StarSubalgebra.mem_top
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
⊢ rng = ⊤
[PROOFSTEP]
have h : rng.topologicalClosure = rng :=
  le_antisymm
    (StarSubalgebra.topologicalClosure_minimal le_rfl (gelfandTransform_isometry A).closedEmbedding.closed_range)
    (StarSubalgebra.le_topologicalClosure _)
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
h : StarSubalgebra.topologicalClosure rng = rng
⊢ rng = ⊤
[PROOFSTEP]
refine'
  h ▸
    ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints _
      (fun _ _ => _)
        /- Separating points just means that elements of the `characterSpace` which agree at all points
            of `A` are the same functional, which is just extensionality. -/
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
h : StarSubalgebra.topologicalClosure rng = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ x✝¹ ≠ x✝ → ∃ f, f ∈ (fun f => ↑f) '' ↑rng.toSubalgebra ∧ f x✝¹ ≠ f x✝
[PROOFSTEP]
contrapose!
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
h : StarSubalgebra.topologicalClosure rng = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ (∀ (f : ↑(characterSpace ℂ A) → ℂ), f ∈ (fun a => ↑a) '' ↑rng.toSubalgebra → f x✝¹ = f x✝) → x✝¹ = x✝
[PROOFSTEP]
exact fun h =>
  Subtype.ext (ContinuousLinearMap.ext fun a => h (gelfandTransform ℂ A a) ⟨gelfandTransform ℂ A a, ⟨a, rfl⟩, rfl⟩)
