[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
⊢ spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rcases subsingleton_or_nontrivial A with ⟨⟩
[GOAL]
case inl
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Subsingleton A
⊢ spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
simp only [spectrum.of_subsingleton, Set.empty_subset]
[GOAL]
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
⊢ spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
set a' : elementalStarAlgebra ℂ a := ⟨a, self_mem ℂ a⟩
[GOAL]
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
refine' (spectrum.subset_starSubalgebra (star a' * a')).trans _
[GOAL]
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ spectrum ℂ (star a' * a') ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rw [← spectrum.gelfandTransform_eq (star a' * a'), ContinuousMap.spectrum_eq_range]
[GOAL]
case inr
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ Set.range ↑(↑(gelfandTransform ℂ { x // x ∈ elementalStarAlgebra ℂ a }) (star a' * a')) ⊆ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rintro - ⟨φ, rfl⟩
[GOAL]
case inr.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
φ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
⊢ ↑(↑(gelfandTransform ℂ { x // x ∈ elementalStarAlgebra ℂ a }) (star a' * a')) φ ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rw [gelfandTransform_apply_apply ℂ _ (star a' * a') φ, map_mul φ, map_star φ]
[GOAL]
case inr.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
φ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
⊢ star (↑φ a') * ↑φ a' ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rw [Complex.eq_coe_norm_of_nonneg (star_mul_self_nonneg _), ← map_star, ← map_mul]
[GOAL]
case inr.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
φ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
⊢ ↑‖↑φ (star a' * a')‖ ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
exact ⟨Complex.zero_le_real.2 (norm_nonneg _), Complex.real_le_real.2 (AlgHom.norm_apply_le_self φ (star a' * a'))⟩
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
⊢ IsUnit { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
⊢ IsUnit { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
[PROOFSTEP]
set a' : elementalStarAlgebra ℂ a := ⟨a, self_mem ℂ a⟩
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ IsUnit a'
[PROOFSTEP]
suffices : IsUnit (star a' * a')
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
this : IsUnit (star a' * a')
⊢ IsUnit a'
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ IsUnit (star a' * a')
[PROOFSTEP]
exact (IsUnit.mul_iff.1 this).2
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
h : IsUnit a
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ IsUnit (star a' * a')
[PROOFSTEP]
replace h :=
  (show Commute (star a) a from star_comm_self' a).isUnit_mul_iff.2
    ⟨h.star, h⟩
      /- Since `a` is invertible, `‖star a * a‖ ≠ 0`, so `‖star a * a‖ • 1` is invertible in
          `elementalStarAlgebra ℂ a`, and so it suffices to show that the distance between this unit and
          `star a * a` is less than `‖star a * a‖`. -/
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
⊢ IsUnit (star a' * a')
[PROOFSTEP]
have h₁ : (‖star a * a‖ : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (norm_ne_zero_iff.mpr h.ne_zero)
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
⊢ IsUnit (star a' * a')
[PROOFSTEP]
set u : Units (elementalStarAlgebra ℂ a) :=
  Units.map (algebraMap ℂ (elementalStarAlgebra ℂ a)).toMonoidHom (Units.mk0 _ h₁)
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
⊢ IsUnit (star a' * a')
[PROOFSTEP]
refine' ⟨u.ofNearby _ _, rfl⟩
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
⊢ ‖star a' * a' - ↑u‖ < ‖↑u⁻¹‖⁻¹
[PROOFSTEP]
simp only [Units.coe_map, Units.val_inv_eq_inv_val, RingHom.toMonoidHom_eq_coe, Units.val_mk0, Units.coe_map_inv,
  MonoidHom.coe_coe, norm_algebraMap', norm_inv, Complex.norm_eq_abs, Complex.abs_ofReal, abs_norm, inv_inv]
  --RingHom.coe_monoidHom,
      -- Complex.abs_ofReal, map_inv₀,
    --rw [norm_algebraMap', inv_inv, Complex.norm_eq_abs, abs_norm]I-
    /- Since `a` is invertible, by `spectrum_star_mul_self_of_isStarNormal`, the spectrum (in `A`)
      of `star a * a` is contained in the half-open interval `(0, ‖star a * a‖]`. Therefore, by basic
      spectral mapping properties, the spectrum of `‖star a * a‖ • 1 - star a * a` is contained in
      `[0, ‖star a * a‖)`. -/
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
⊢ ‖star { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } *
          { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } -
        ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a }) ↑‖star a * a‖‖ <
    ‖star a * a‖
[PROOFSTEP]
have h₂ : ∀ z ∈ spectrum ℂ (algebraMap ℂ A ‖star a * a‖ - star a * a), ‖z‖₊ < ‖star a * a‖₊ :=
  by
  intro z hz
  rw [← spectrum.singleton_sub_eq, Set.singleton_sub] at hz 
  have h₃ : z ∈ Set.Icc (0 : ℂ) ‖star a * a‖ :=
    by
    replace hz := Set.image_subset _ (spectrum_star_mul_self_of_isStarNormal a) hz
    rwa [Set.image_const_sub_Icc, sub_self, sub_zero] at hz 
  refine' lt_of_le_of_ne (Complex.real_le_real.1 <| Complex.eq_coe_norm_of_nonneg h₃.1 ▸ h₃.2) _
  · intro hz'
    replace hz' := congr_arg (fun x : ℝ≥0 => ((x : ℝ) : ℂ)) hz'
    simp only [coe_nnnorm] at hz' 
    rw [← Complex.eq_coe_norm_of_nonneg h₃.1] at hz' 
    obtain ⟨w, hw₁, hw₂⟩ := hz
    refine' (spectrum.zero_not_mem_iff ℂ).mpr h _
    rw [hz', sub_eq_self] at hw₂ 
    rwa [hw₂] at hw₁ 
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
⊢ ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
[PROOFSTEP]
intro z hz
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a)
⊢ ‖z‖₊ < ‖star a * a‖₊
[PROOFSTEP]
rw [← spectrum.singleton_sub_eq, Set.singleton_sub] at hz 
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
⊢ ‖z‖₊ < ‖star a * a‖₊
[PROOFSTEP]
have h₃ : z ∈ Set.Icc (0 : ℂ) ‖star a * a‖ :=
  by
  replace hz := Set.image_subset _ (spectrum_star_mul_self_of_isStarNormal a) hz
  rwa [Set.image_const_sub_Icc, sub_self, sub_zero] at hz 
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
⊢ z ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
replace hz := Set.image_subset _ (spectrum_star_mul_self_of_isStarNormal a) hz
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' Set.Icc 0 ↑‖star a * a‖
⊢ z ∈ Set.Icc 0 ↑‖star a * a‖
[PROOFSTEP]
rwa [Set.image_const_sub_Icc, sub_self, sub_zero] at hz 
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
⊢ ‖z‖₊ < ‖star a * a‖₊
[PROOFSTEP]
refine' lt_of_le_of_ne (Complex.real_le_real.1 <| Complex.eq_coe_norm_of_nonneg h₃.1 ▸ h₃.2) _
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
⊢ ‖z‖₊ ≠ ‖star a * a‖₊
[PROOFSTEP]
intro hz'
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : ‖z‖₊ = ‖star a * a‖₊
⊢ False
[PROOFSTEP]
replace hz' := congr_arg (fun x : ℝ≥0 => ((x : ℝ) : ℂ)) hz'
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : (fun x => ↑↑x) ‖z‖₊ = (fun x => ↑↑x) ‖star a * a‖₊
⊢ False
[PROOFSTEP]
simp only [coe_nnnorm] at hz' 
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : ↑‖z‖ = ↑‖star a * a‖
⊢ False
[PROOFSTEP]
rw [← Complex.eq_coe_norm_of_nonneg h₃.1] at hz' 
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
hz : z ∈ (fun x x_1 => x - x_1) ↑‖star a * a‖ '' spectrum ℂ (star a * a)
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : z = ↑‖star a * a‖
⊢ False
[PROOFSTEP]
obtain ⟨w, hw₁, hw₂⟩ := hz
[GOAL]
case intro.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : z = ↑‖star a * a‖
w : ℂ
hw₁ : w ∈ spectrum ℂ (star a * a)
hw₂ : (fun x x_1 => x - x_1) (↑‖star a * a‖) w = z
⊢ False
[PROOFSTEP]
refine' (spectrum.zero_not_mem_iff ℂ).mpr h _
[GOAL]
case intro.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : z = ↑‖star a * a‖
w : ℂ
hw₁ : w ∈ spectrum ℂ (star a * a)
hw₂ : (fun x x_1 => x - x_1) (↑‖star a * a‖) w = z
⊢ 0 ∈ spectrum ℂ (star a * a)
[PROOFSTEP]
rw [hz', sub_eq_self] at hw₂ 
[GOAL]
case intro.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
z : ℂ
h₃ : z ∈ Set.Icc 0 ↑‖star a * a‖
hz' : z = ↑‖star a * a‖
w : ℂ
hw₁ : w ∈ spectrum ℂ (star a * a)
hw₂ : w = 0
⊢ 0 ∈ spectrum ℂ (star a * a)
[PROOFSTEP]
rwa [hw₂] at hw₁ 
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ‖star { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } *
          { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } -
        ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a }) ↑‖star a * a‖‖ <
    ‖star a * a‖
[PROOFSTEP]
exact
  ENNReal.coe_lt_coe.1
    (calc
      (‖star a' * a' - algebraMap ℂ _ ‖star a * a‖‖₊ : ℝ≥0∞) = ‖algebraMap ℂ A ‖star a * a‖ - star a * a‖₊ := by
        rw [← nnnorm_neg, neg_sub]; rfl
      _ = spectralRadius ℂ (algebraMap ℂ A ‖star a * a‖ - star a * a) :=
        by
        refine' (IsSelfAdjoint.spectralRadius_eq_nnnorm _).symm
        rw [IsSelfAdjoint, star_sub, star_mul, star_star, ← algebraMap_star_comm]
        congr!
        exact IsROrC.conj_ofReal _
      _ < ‖star a * a‖₊ := spectrum.spectralRadius_lt_of_forall_lt _ h₂)
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ↑‖star a' * a' - ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a }) ↑‖star a * a‖‖₊ =
    ↑‖↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a‖₊
[PROOFSTEP]
rw [← nnnorm_neg, neg_sub]
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ↑‖↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a }) ↑‖star a * a‖ - star a' * a'‖₊ =
    ↑‖↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a‖₊
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ↑‖↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a‖₊ = spectralRadius ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a)
[PROOFSTEP]
refine' (IsSelfAdjoint.spectralRadius_eq_nnnorm _).symm
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ IsSelfAdjoint (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a)
[PROOFSTEP]
rw [IsSelfAdjoint, star_sub, star_mul, star_star, ← algebraMap_star_comm]
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ ↑(algebraMap ℂ A) (star ↑‖star a * a‖) - star a * a = ↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a
[PROOFSTEP]
congr!
[GOAL]
case h.e'_5.h.e'_6
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
✝ : Nontrivial A
a' : { x // x ∈ elementalStarAlgebra ℂ a } := { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
h : IsUnit (star a * a)
h₁ : ↑‖star a * a‖ ≠ 0
u : { x // x ∈ elementalStarAlgebra ℂ a }ˣ :=
  ↑(Units.map ↑(algebraMap ℂ { x // x ∈ elementalStarAlgebra ℂ a })) (Units.mk0 (↑‖star a * a‖) h₁)
h₂ : ∀ (z : ℂ), z ∈ spectrum ℂ (↑(algebraMap ℂ A) ↑‖star a * a‖ - star a * a) → ‖z‖₊ < ‖star a * a‖₊
⊢ star ↑‖star a * a‖ = ↑‖star a * a‖
[PROOFSTEP]
exact IsROrC.conj_ofReal _
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
⊢ ↑(IsUnit.unit h)⁻¹ ∈ S
[PROOFSTEP]
have hx := h.star.mul h
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
⊢ ↑(IsUnit.unit h)⁻¹ ∈ S
[PROOFSTEP]
suffices this : (↑hx.unit⁻¹ : A) ∈ S
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : ↑(IsUnit.unit hx)⁻¹ ∈ S
⊢ ↑(IsUnit.unit h)⁻¹ ∈ S
[PROOFSTEP]
rw [← one_mul (↑h.unit⁻¹ : A), ← hx.unit.inv_mul, mul_assoc, IsUnit.unit_spec, mul_assoc, h.mul_val_inv, mul_one]
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : ↑(IsUnit.unit hx)⁻¹ ∈ S
⊢ ↑(IsUnit.unit hx)⁻¹ * star x ∈ S
[PROOFSTEP]
exact mul_mem this (star_mem hxS)
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
⊢ ↑(IsUnit.unit hx)⁻¹ ∈ S
[PROOFSTEP]
refine' le_of_isClosed_of_mem ℂ hS (mul_mem (star_mem hxS) hxS) _
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
⊢ ↑(IsUnit.unit hx)⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
[PROOFSTEP]
haveI := (IsSelfAdjoint.star_mul_self x).isStarNormal
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : IsStarNormal (star x * x)
⊢ ↑(IsUnit.unit hx)⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
[PROOFSTEP]
have hx' := elementalStarAlgebra.isUnit_of_isUnit_of_isStarNormal hx
[GOAL]
case this
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : IsStarNormal (star x * x)
hx' : IsUnit { val := star x * x, property := (_ : star x * x ∈ elementalStarAlgebra ℂ (star x * x)) }
⊢ ↑(IsUnit.unit hx)⁻¹ ∈ elementalStarAlgebra ℂ (star x * x)
[PROOFSTEP]
convert (↑hx'.unit⁻¹ : elementalStarAlgebra ℂ (star x * x)).prop using 1
[GOAL]
case h.e'_4
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : IsStarNormal (star x * x)
hx' : IsUnit { val := star x * x, property := (_ : star x * x ∈ elementalStarAlgebra ℂ (star x * x)) }
⊢ ↑(IsUnit.unit hx)⁻¹ = ↑↑(IsUnit.unit hx')⁻¹
[PROOFSTEP]
refine left_inv_eq_right_inv hx.unit.inv_mul ?_
[GOAL]
case h.e'_4
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : A
h : IsUnit x
hxS : x ∈ S
hx : IsUnit (star x * x)
this : IsStarNormal (star x * x)
hx' : IsUnit { val := star x * x, property := (_ : star x * x ∈ elementalStarAlgebra ℂ (star x * x)) }
⊢ ↑(IsUnit.unit hx) * ↑↑(IsUnit.unit hx')⁻¹ = 1
[PROOFSTEP]
exact (congr_arg ((↑) : _ → A) hx'.unit.mul_inv)
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : { x // x ∈ S }
⊢ IsUnit ↑x ↔ IsUnit x
[PROOFSTEP]
refine'
  ⟨fun hx => ⟨⟨x, ⟨(↑hx.unit⁻¹ : A), StarSubalgebra.isUnit_coe_inv_mem hS hx x.prop⟩, _, _⟩, rfl⟩, fun hx =>
    hx.map S.subtype⟩
[GOAL]
case refine'_1
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : { x // x ∈ S }
hx : IsUnit ↑x
⊢ x * { val := ↑(IsUnit.unit hx)⁻¹, property := (_ : ↑(IsUnit.unit hx)⁻¹ ∈ S) } = 1
case refine'_2
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S✝ S : StarSubalgebra ℂ A
hS : IsClosed ↑S
x : { x // x ∈ S }
hx : IsUnit ↑x
⊢ { val := ↑(IsUnit.unit hx)⁻¹, property := (_ : ↑(IsUnit.unit hx)⁻¹ ∈ S) } * x = 1
[PROOFSTEP]
exacts [Subtype.coe_injective hx.mul_val_inv, Subtype.coe_injective hx.val_inv_mul]
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
x : A
φ : ↑(characterSpace ℂ { x_1 // x_1 ∈ elementalStarAlgebra ℂ x })
⊢ ↑φ { val := x, property := (_ : x ∈ elementalStarAlgebra ℂ x) } ∈ spectrum ℂ x
[PROOFSTEP]
simpa only [StarSubalgebra.spectrum_eq (elementalStarAlgebra.isClosed ℂ x) ⟨x, self_mem ℂ x⟩] using
  AlgHom.apply_mem_spectrum φ ⟨x, self_mem ℂ x⟩
[GOAL]
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
⊢ Function.Bijective (characterSpaceToSpectrum a)
[PROOFSTEP]
refine' ⟨fun φ ψ h => starAlgHomClass_ext ℂ _ _ _, _⟩
[GOAL]
case refine'_1
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
φ ψ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ↑φ
[PROOFSTEP]
exact (map_continuous φ)
[GOAL]
case refine'_2
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
φ ψ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ↑ψ
[PROOFSTEP]
exact (map_continuous ψ)
[GOAL]
case refine'_3
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
φ ψ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
[PROOFSTEP]
simpa only [elementalStarAlgebra.characterSpaceToSpectrum, Subtype.mk_eq_mk, ContinuousMap.coe_mk] using h
[GOAL]
case refine'_4
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
⊢ Function.Surjective (characterSpaceToSpectrum a)
[PROOFSTEP]
rintro ⟨z, hz⟩
[GOAL]
case refine'_4.mk
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = { val := z, property := hz }
[PROOFSTEP]
have hz' := (StarSubalgebra.spectrum_eq (elementalStarAlgebra.isClosed ℂ a) ⟨a, self_mem ℂ a⟩).symm.subst hz
[GOAL]
case refine'_4.mk
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : z ∈ spectrum ℂ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = { val := z, property := hz }
[PROOFSTEP]
rw [CharacterSpace.mem_spectrum_iff_exists] at hz' 
[GOAL]
case refine'_4.mk
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : ∃ f, ↑f { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } = z
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = { val := z, property := hz }
[PROOFSTEP]
obtain ⟨φ, rfl⟩ := hz'
[GOAL]
case refine'_4.mk.intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : NormedAlgebra ℂ A
inst✝⁴ : StarRing A
inst✝³ : CstarRing A
inst✝² : StarModule ℂ A
inst✝¹ : CompleteSpace A
a : A
inst✝ : IsStarNormal a
S : StarSubalgebra ℂ A
φ : ↑(characterSpace ℂ { x // x ∈ elementalStarAlgebra ℂ a })
hz : ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) } ∈ spectrum ℂ a
⊢ ∃ a_1,
    characterSpaceToSpectrum a a_1 =
      { val := ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra ℂ a) }, property := hz }
[PROOFSTEP]
exact ⟨φ, rfl⟩
