[GOAL]
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
⊢ spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1
[PROOFSTEP]
nontriviality E
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
⊢ spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1
[PROOFSTEP]
refine' fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm _ _)
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k ∈ spectrum 𝕜 ↑u
⊢ ‖k‖ ≤ 1
[PROOFSTEP]
simpa only [CstarRing.norm_coe_unitary u] using norm_le_norm_of_mem hk
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k ∈ spectrum 𝕜 ↑u
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
rw [← unitary.toUnits_apply_val u] at hk 
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k ∈ spectrum 𝕜 ↑(↑toUnits u)
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
have hnk := ne_zero_of_mem_of_unit hk
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k ∈ spectrum 𝕜 ↑(↑toUnits u)
hnk : k ≠ 0
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
rw [← inv_inv (unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk 
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ spectrum 𝕜 ↑(↑toUnits u)⁻¹
hnk : k ≠ 0
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
have : ‖k‖⁻¹ ≤ ‖(↑(unitary.toUnits u)⁻¹ : E)‖ := by simpa only [norm_inv] using norm_le_norm_of_mem hk
[GOAL]
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ spectrum 𝕜 ↑(↑toUnits u)⁻¹
hnk : k ≠ 0
⊢ ‖k‖⁻¹ ≤ ‖↑(↑toUnits u)⁻¹‖
[PROOFSTEP]
simpa only [norm_inv] using norm_le_norm_of_mem hk
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CstarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : { x // x ∈ unitary E }
✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ spectrum 𝕜 ↑(↑toUnits u)⁻¹
hnk : k ≠ 0
this : ‖k‖⁻¹ ≤ ‖↑(↑toUnits u)⁻¹‖
⊢ 1 ≤ ‖k‖
[PROOFSTEP]
simpa [← Units.inv_eq_val_inv] using inv_le_of_inv_le (norm_pos_iff.mpr hnk) this
[GOAL]
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
⊢ spectralRadius ℂ a = ↑‖a‖₊
[PROOFSTEP]
have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds
[GOAL]
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ spectralRadius ℂ a = ↑‖a‖₊
[PROOFSTEP]
refine' tendsto_nhds_unique _ hconst
[GOAL]
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 (spectralRadius ℂ a))
[PROOFSTEP]
convert
  (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
    (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using
  1
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ (fun _n => ↑‖a‖₊) = (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n
[PROOFSTEP]
refine' funext fun n => _
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ((fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n) n
[PROOFSTEP]
rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_nat_cast, ← rpow_mul]
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra ℂ A
inst✝² : CompleteSpace A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ↑‖a‖₊ ^ (↑(2 ^ n) * (1 / ↑(2 ^ n)))
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
⊢ spectralRadius ℂ a = ↑‖a‖₊
[PROOFSTEP]
refine' (ENNReal.pow_strictMono two_ne_zero).injective _
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
[PROOFSTEP]
have heq :
  (fun n : ℕ => (‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) =
    (fun x => x ^ 2) ∘ fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ) :=
  by
  funext n
  rw [Function.comp_apply, ← rpow_nat_cast, ← rpow_mul, mul_comm, rpow_mul, rpow_nat_cast, ← coe_pow, sq, ←
    nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
⊢ (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
[PROOFSTEP]
funext n
[GOAL]
case h
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
n : ℕ
⊢ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n) = ((fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) n
[PROOFSTEP]
rw [Function.comp_apply, ← rpow_nat_cast, ← rpow_mul, mul_comm, rpow_mul, rpow_nat_cast, ← coe_pow, sq, ←
  nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
[PROOFSTEP]
have h₂ :=
  ((ENNReal.continuous_pow 2).tendsto (spectralRadius ℂ a)).comp
    (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a)
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto ((fun a => a ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
[PROOFSTEP]
rw [← heq] at h₂ 
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
[PROOFSTEP]
convert tendsto_nhds_unique h₂ (pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a⋆ * a))
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
a : A
inst✝ : IsStarNormal a
heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ ↑‖a‖₊ ^ 2 = spectralRadius ℂ (a⋆ * a)
[PROOFSTEP]
rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_mul]
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ z = ↑z.re
[PROOFSTEP]
have hu := exp_mem_unitary_of_mem_skewAdjoint ℂ (ha.smul_mem_skewAdjoint conj_I)
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
⊢ z = ↑z.re
[PROOFSTEP]
let Iu := Units.mk0 I I_ne_zero
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
⊢ z = ↑z.re
[PROOFSTEP]
have : _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.exp ℂ (I • a)) := by
  simpa only [Units.smul_def, Units.val_mk0] using spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
⊢ _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.exp ℂ (I • a))
[PROOFSTEP]
simpa only [Units.smul_def, Units.val_mk0] using spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.exp ℂ (I • a))
⊢ z = ↑z.re
[PROOFSTEP]
exact
  Complex.ext (ofReal_re _) <| by
    simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_eq_abs, abs_exp, Real.exp_eq_one_iff,
      smul_eq_mul, I_mul, neg_eq_zero] using spectrum.subset_circle_of_unitary hu this
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
hu : _root_.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.exp ℂ (I • a))
⊢ z.im = (↑z.re).im
[PROOFSTEP]
simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_eq_abs, abs_exp, Real.exp_eq_one_iff, smul_eq_mul,
  I_mul, neg_eq_zero] using spectrum.subset_circle_of_unitary hu this
[GOAL]
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
⊢ z ∈ ofReal' ∘ re '' spectrum ℂ a → z ∈ spectrum ℂ a
[PROOFSTEP]
rintro ⟨z, hz, rfl⟩
[GOAL]
case intro.intro
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ (ofReal' ∘ re) z ∈ spectrum ℂ a
[PROOFSTEP]
simpa only [(ha.mem_spectrum_eq_re hz).symm, Function.comp_apply] using hz
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a : A
⊢ ‖↑φ a‖₊ ≤ ‖a‖₊
[PROOFSTEP]
suffices ∀ s : A, IsSelfAdjoint s → ‖φ s‖₊ ≤ ‖s‖₊ by
  exact
    nonneg_le_nonneg_of_sq_le_sq zero_le' <| by
      simpa only [nnnorm_star_mul_self, map_star, map_mul] using this _ (IsSelfAdjoint.star_mul_self a)
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a : A
this : ∀ (s : A), IsSelfAdjoint s → ‖↑φ s‖₊ ≤ ‖s‖₊
⊢ ‖↑φ a‖₊ ≤ ‖a‖₊
[PROOFSTEP]
exact
  nonneg_le_nonneg_of_sq_le_sq zero_le' <| by
    simpa only [nnnorm_star_mul_self, map_star, map_mul] using this _ (IsSelfAdjoint.star_mul_self a)
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a : A
this : ∀ (s : A), IsSelfAdjoint s → ‖↑φ s‖₊ ≤ ‖s‖₊
⊢ ‖↑φ a‖₊ * ‖↑φ a‖₊ ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simpa only [nnnorm_star_mul_self, map_star, map_mul] using this _ (IsSelfAdjoint.star_mul_self a)
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a : A
⊢ ∀ (s : A), IsSelfAdjoint s → ‖↑φ s‖₊ ≤ ‖s‖₊
[PROOFSTEP]
intro s hs
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ : F
a s : A
hs : IsSelfAdjoint s
⊢ ‖↑φ s‖₊ ≤ ‖s‖₊
[PROOFSTEP]
simpa only [hs.spectralRadius_eq_nnnorm, (hs.starHom_apply φ).spectralRadius_eq_nnnorm, coe_le_coe] using
  show spectralRadius ℂ (φ s) ≤ spectralRadius ℂ s from iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset φ s)
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : NormedRing A
inst✝⁸ : NormedAlgebra ℂ A
inst✝⁷ : CompleteSpace A
inst✝⁶ : StarRing A
inst✝⁵ : CstarRing A
inst✝⁴ : NormedRing B
inst✝³ : NormedAlgebra ℂ B
inst✝² : CompleteSpace B
inst✝¹ : StarRing B
inst✝ : CstarRing B
hF : StarAlgHomClass F ℂ A B
φ✝ : F
src✝ : LinearMapClass F ℂ A B := AlgHomClass.linearMapClass
φ : F
⊢ ∀ (x : A), ‖↑φ x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simpa only [one_mul] using nnnorm_apply_le φ
[GOAL]
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
⊢ ↑φ a⋆ = (↑φ a)⋆
[PROOFSTEP]
suffices hsa : ∀ s : selfAdjoint A, (φ s)⋆ = φ s
[GOAL]
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
hsa : ∀ (s : { x // x ∈ selfAdjoint A }), (↑φ ↑s)⋆ = ↑φ ↑s
⊢ ↑φ a⋆ = (↑φ a)⋆
[PROOFSTEP]
rw [← realPart_add_I_smul_imaginaryPart a]
[GOAL]
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
hsa : ∀ (s : { x // x ∈ selfAdjoint A }), (↑φ ↑s)⋆ = ↑φ ↑s
⊢ ↑φ (↑(↑ℜ a) + I • ↑(↑ℑ a))⋆ = (↑φ (↑(↑ℜ a) + I • ↑(↑ℑ a)))⋆
[PROOFSTEP]
simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq]
[GOAL]
case hsa
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
⊢ ∀ (s : { x // x ∈ selfAdjoint A }), (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
intro s
[GOAL]
case hsa
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
have := AlgHom.apply_mem_spectrum φ (s : A)
[GOAL]
case hsa
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
this : ↑φ ↑s ∈ spectrum ℂ ↑s
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
rw [selfAdjoint.val_re_map_spectrum s] at this 
[GOAL]
case hsa
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
this : ↑φ ↑s ∈ ofReal' ∘ re '' spectrum ℂ ↑s
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
rcases this with ⟨⟨_, _⟩, _, heq⟩
[GOAL]
case hsa.intro.mk.intro
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
re✝ im✝ : ℝ
left✝ : { re := re✝, im := im✝ } ∈ spectrum ℂ ↑s
heq : (ofReal' ∘ re) { re := re✝, im := im✝ } = ↑φ ↑s
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
simp only [Function.comp_apply] at heq 
[GOAL]
case hsa.intro.mk.intro
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
re✝ im✝ : ℝ
left✝ : { re := re✝, im := im✝ } ∈ spectrum ℂ ↑s
heq : ↑re✝ = ↑φ ↑s
⊢ (↑φ ↑s)⋆ = ↑φ ↑s
[PROOFSTEP]
rw [← heq, IsROrC.star_def]
[GOAL]
case hsa.intro.mk.intro
F : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : { x // x ∈ selfAdjoint A }
re✝ im✝ : ℝ
left✝ : { re := re✝, im := im✝ } ∈ spectrum ℂ ↑s
heq : ↑re✝ = ↑φ ↑s
⊢ ↑(starRingEnd ((fun x => ℂ) ↑s)) ↑re✝ = ↑re✝
[PROOFSTEP]
exact IsROrC.conj_ofReal _
