[GOAL]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ IsConformalMap f ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f u) (↑f v) = c * inner u v
[PROOFSTEP]
constructor
[GOAL]
case mp
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ IsConformalMap f → ∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f u) (↑f v) = c * inner u v
[PROOFSTEP]
rintro ⟨c₁, hc₁, li, rfl⟩
[GOAL]
case mp.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ ∃ c,
    0 < c ∧ ∀ (u v : E), inner (↑(c₁ • toContinuousLinearMap li) u) (↑(c₁ • toContinuousLinearMap li) v) = c * inner u v
[PROOFSTEP]
refine' ⟨c₁ * c₁, mul_self_pos.2 hc₁, fun u v => _⟩
[GOAL]
case mp.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
u v : E
⊢ inner (↑(c₁ • toContinuousLinearMap li) u) (↑(c₁ • toContinuousLinearMap li) v) = c₁ * c₁ * inner u v
[PROOFSTEP]
simp only [real_inner_smul_left, real_inner_smul_right, mul_assoc, coe_smul', coe_toContinuousLinearMap, Pi.smul_apply,
  inner_map_map]
[GOAL]
case mpr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ (∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f u) (↑f v) = c * inner u v) → IsConformalMap f
[PROOFSTEP]
rintro ⟨c₁, hc₁, huv⟩
[GOAL]
case mpr.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c₁ * inner u v
⊢ IsConformalMap f
[PROOFSTEP]
obtain ⟨c, hc, rfl⟩ : ∃ c : ℝ, 0 < c ∧ c₁ = c * c
[GOAL]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c₁ * inner u v
⊢ ∃ c, 0 < c ∧ c₁ = c * c
case mpr.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ IsConformalMap f
[PROOFSTEP]
exact ⟨Real.sqrt c₁, Real.sqrt_pos.2 hc₁, (Real.mul_self_sqrt hc₁.le).symm⟩
[GOAL]
case mpr.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ IsConformalMap f
[PROOFSTEP]
refine' ⟨c, hc.ne', (c⁻¹ • f : E →ₗ[ℝ] F).isometryOfInner fun u v => _, _⟩
[GOAL]
case mpr.intro.intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
u v : E
⊢ inner (↑↑(c⁻¹ • f) u) (↑↑(c⁻¹ • f) v) = inner u v
[PROOFSTEP]
simp only [real_inner_smul_left, real_inner_smul_right, huv, mul_assoc, coe_smul, inv_mul_cancel_left₀ hc.ne',
  LinearMap.smul_apply, ContinuousLinearMap.coe_coe]
[GOAL]
case mpr.intro.intro.intro.intro.refine'_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ f =
    c •
      toContinuousLinearMap
        (LinearMap.isometryOfInner ↑(c⁻¹ • f) (_ : ∀ (u v : E), inner (c⁻¹ • ↑f u) (c⁻¹ • ↑f v) = inner u v))
[PROOFSTEP]
ext1 x
[GOAL]
case mpr.intro.intro.intro.intro.refine'_2.h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
x : E
⊢ ↑f x =
    ↑(c •
          toContinuousLinearMap
            (LinearMap.isometryOfInner ↑(c⁻¹ • f) (_ : ∀ (u v : E), inner (c⁻¹ • ↑f u) (c⁻¹ • ↑f v) = inner u v)))
      x
[PROOFSTEP]
exact (smul_inv_smul₀ hc.ne' (f x)).symm


[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ ∀ (x : E), ‖↑0 x‖ ≤ 0 * ‖x‖
[PROOFSTEP]
simp [le_refl]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ ∀ (x : E), ‖↑LinearMap.id x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simp [le_refl]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ IsBoundedLinearMap 𝕜 fun x => x.fst
[PROOFSTEP]
refine' (LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => _
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E × F
⊢ ‖↑(LinearMap.fst 𝕜 E F) x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
rw [one_mul]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E × F
⊢ ‖↑(LinearMap.fst 𝕜 E F) x‖ ≤ ‖x‖
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ IsBoundedLinearMap 𝕜 fun x => x.snd
[PROOFSTEP]
refine' (LinearMap.snd 𝕜 E F).isLinear.with_bound 1 fun x => _
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E × F
⊢ ‖↑(LinearMap.snd 𝕜 E F) x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
rw [one_mul]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E × F
⊢ ‖↑(LinearMap.snd 𝕜 E F) x‖ ≤ ‖x‖
[PROOFSTEP]
exact le_max_right _ _
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ IsBoundedLinearMap 𝕜 fun e => -f e
[PROOFSTEP]
rw [show (fun e => -f e) = fun e => (-1 : 𝕜) • f e by funext; simp]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ (fun e => -f e) = fun e => -1 • f e
[PROOFSTEP]
funext
[GOAL]
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
x✝ : E
⊢ -f x✝ = -1 • f x✝
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ IsBoundedLinearMap 𝕜 fun e => -1 • f e
[PROOFSTEP]
exact smul (-1) hf
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left✝¹ : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left✝ : 0 < Mg
hMg : ∀ (x : E), ‖g x‖ ≤ Mg * ‖x‖
x : E
⊢ Mf * ‖x‖ + Mg * ‖x‖ ≤ (Mf + Mg) * ‖x‖
[PROOFSTEP]
rw [add_mul]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
⊢ IsBoundedLinearMap 𝕜 fun e => f e - g e
[PROOFSTEP]
simpa [sub_eq_add_neg] using add hf (neg hg)
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
x : E
hf✝ : IsBoundedLinearMap 𝕜 f
hf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
e : E
⊢ ‖f e - f x‖ = ‖↑(IsLinearMap.mk' f hf) (e - x)‖
[PROOFSTEP]
rw [(hf.mk' _).map_sub e x]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
x : E
hf✝ : IsBoundedLinearMap 𝕜 f
hf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
e : E
⊢ ‖f e - f x‖ = ‖↑(IsLinearMap.mk' f hf) e - ↑(IsLinearMap.mk' f hf) x‖
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
x : E
hf✝ : IsBoundedLinearMap 𝕜 f
hf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
this : Tendsto (fun e => M * ‖e - x‖) (𝓝 x) (𝓝 (M * 0))
⊢ Tendsto (fun e => M * ‖e - x‖) (𝓝 x) (𝓝 0)
[PROOFSTEP]
simpa
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p₁ p₂ : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
⊢ ContinuousMultilinearMap.prod (p₁ + p₂).fst (p₁ + p₂).snd =
    ContinuousMultilinearMap.prod p₁.fst p₁.snd + ContinuousMultilinearMap.prod p₂.fst p₂.snd
[PROOFSTEP]
ext1 m
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p₁ p₂ : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ↑(ContinuousMultilinearMap.prod (p₁ + p₂).fst (p₁ + p₂).snd) m =
    ↑(ContinuousMultilinearMap.prod p₁.fst p₁.snd + ContinuousMultilinearMap.prod p₂.fst p₂.snd) m
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
c : 𝕜
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
⊢ ContinuousMultilinearMap.prod (c • p).fst (c • p).snd = c • ContinuousMultilinearMap.prod p.fst p.snd
[PROOFSTEP]
ext1 m
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
c : 𝕜
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ↑(ContinuousMultilinearMap.prod (c • p).fst (c • p).snd) m = ↑(c • ContinuousMultilinearMap.prod p.fst p.snd) m
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
⊢ ‖ContinuousMultilinearMap.prod p.fst p.snd‖ ≤ 1 * ‖p‖
[PROOFSTEP]
rw [one_mul]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
⊢ ‖ContinuousMultilinearMap.prod p.fst p.snd‖ ≤ ‖p‖
[PROOFSTEP]
apply ContinuousMultilinearMap.op_norm_le_bound _ (norm_nonneg _) _
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
⊢ ∀ (m : (i : ι) → E i), ‖↑(ContinuousMultilinearMap.prod p.fst p.snd) m‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖
[PROOFSTEP]
intro m
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖↑(ContinuousMultilinearMap.prod p.fst p.snd) m‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖
[PROOFSTEP]
rw [ContinuousMultilinearMap.prod_apply, norm_prod_le_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖(↑p.fst m, ↑p.snd m).fst‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖ ∧ ‖(↑p.fst m, ↑p.snd m).snd‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖
[PROOFSTEP]
constructor
[GOAL]
case left
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖(↑p.fst m, ↑p.snd m).fst‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖
[PROOFSTEP]
exact
  (p.1.le_op_norm m).trans (mul_le_mul_of_nonneg_right (norm_fst_le p) (Finset.prod_nonneg fun i _ => norm_nonneg _))
[GOAL]
case right
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
inst✝² : Fintype ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖(↑p.fst m, ↑p.snd m).snd‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖
[PROOFSTEP]
exact
  (p.2.le_op_norm m).trans (mul_le_mul_of_nonneg_right (norm_snd_le p) (Finset.prod_nonneg fun i _ => norm_nonneg _))
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
⊢ IsBoundedLinearMap 𝕜 fun f => ContinuousMultilinearMap.compContinuousLinearMap f fun x => g
[PROOFSTEP]
refine' IsLinearMap.with_bound ⟨fun f₁ f₂ => by ext; rfl, fun c f => by ext; rfl⟩ (‖g‖ ^ Fintype.card ι) fun f => _
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f₁ f₂ : ContinuousMultilinearMap 𝕜 (fun x => E) F
⊢ (ContinuousMultilinearMap.compContinuousLinearMap (f₁ + f₂) fun x => g) =
    (ContinuousMultilinearMap.compContinuousLinearMap f₁ fun x => g) +
      ContinuousMultilinearMap.compContinuousLinearMap f₂ fun x => g
[PROOFSTEP]
ext
[GOAL]
case H
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f₁ f₂ : ContinuousMultilinearMap 𝕜 (fun x => E) F
x✝ : ι → G
⊢ ↑(ContinuousMultilinearMap.compContinuousLinearMap (f₁ + f₂) fun x => g) x✝ =
    ↑((ContinuousMultilinearMap.compContinuousLinearMap f₁ fun x => g) +
          ContinuousMultilinearMap.compContinuousLinearMap f₂ fun x => g)
      x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
c : 𝕜
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
⊢ (ContinuousMultilinearMap.compContinuousLinearMap (c • f) fun x => g) =
    c • ContinuousMultilinearMap.compContinuousLinearMap f fun x => g
[PROOFSTEP]
ext
[GOAL]
case H
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
c : 𝕜
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
x✝ : ι → G
⊢ ↑(ContinuousMultilinearMap.compContinuousLinearMap (c • f) fun x => g) x✝ =
    ↑(c • ContinuousMultilinearMap.compContinuousLinearMap f fun x => g) x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
⊢ ‖ContinuousMultilinearMap.compContinuousLinearMap f fun x => g‖ ≤ ‖g‖ ^ Fintype.card ι * ‖f‖
[PROOFSTEP]
apply ContinuousMultilinearMap.op_norm_le_bound _ _ _
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
⊢ 0 ≤ ‖g‖ ^ Fintype.card ι * ‖f‖
[PROOFSTEP]
apply_rules [mul_nonneg, pow_nonneg, norm_nonneg]
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
⊢ ∀ (m : ι → G),
    ‖↑(ContinuousMultilinearMap.compContinuousLinearMap f fun x => g) m‖ ≤ ‖g‖ ^ Fintype.card ι * ‖f‖ * ∏ i : ι, ‖m i‖
[PROOFSTEP]
intro m
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
m : ι → G
⊢ ‖↑(ContinuousMultilinearMap.compContinuousLinearMap f fun x => g) m‖ ≤ ‖g‖ ^ Fintype.card ι * ‖f‖ * ∏ i : ι, ‖m i‖
[PROOFSTEP]
calc
  ‖f (g ∘ m)‖ ≤ ‖f‖ * ∏ i, ‖g (m i)‖ := f.le_op_norm _
  _ ≤ ‖f‖ * ∏ i, ‖g‖ * ‖m i‖ := by
    apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
    exact Finset.prod_le_prod (fun i _ => norm_nonneg _) fun i _ => g.le_op_norm _
  _ = ‖g‖ ^ Fintype.card ι * ‖f‖ * ∏ i, ‖m i‖ :=
    by
    simp [Finset.prod_mul_distrib, Finset.card_univ]
    ring
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
m : ι → G
⊢ ‖f‖ * ∏ i : ι, ‖↑g (m i)‖ ≤ ‖f‖ * ∏ i : ι, ‖g‖ * ‖m i‖
[PROOFSTEP]
apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
m : ι → G
⊢ ∏ i : ι, ‖↑g (m i)‖ ≤ ∏ i : ι, ‖g‖ * ‖m i‖
[PROOFSTEP]
exact Finset.prod_le_prod (fun i _ => norm_nonneg _) fun i _ => g.le_op_norm _
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
m : ι → G
⊢ ‖f‖ * ∏ i : ι, ‖g‖ * ‖m i‖ = ‖g‖ ^ Fintype.card ι * ‖f‖ * ∏ i : ι, ‖m i‖
[PROOFSTEP]
simp [Finset.prod_mul_distrib, Finset.card_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
ι : Type u_5
inst✝ : Fintype ι
g : G →L[𝕜] E
f : ContinuousMultilinearMap 𝕜 (fun x => E) F
m : ι → G
⊢ ‖f‖ * (‖g‖ ^ Fintype.card ι * ∏ x : ι, ‖m x‖) = ‖g‖ ^ Fintype.card ι * ‖f‖ * ∏ x : ι, ‖m x‖
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace 𝕜 G
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
x x' : M
y : F
⊢ ↑(↑f (x + x')) y = ↑(↑f x) y + ↑(↑f x') y
[PROOFSTEP]
rw [f.map_add, add_apply]
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace 𝕜 G
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
y : F
⊢ ↑(↑f 0) y = 0
[PROOFSTEP]
rw [f.map_zero, zero_apply]
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace 𝕜 G
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
c : R
x : M
y : F
⊢ ↑(↑f (c • x)) y = ↑ρ₁₂ c • ↑(↑f x) y
[PROOFSTEP]
rw [f.map_smulₛₗ, smul_apply]
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace 𝕜 G
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
x x' : M
y : F
⊢ ↑(↑f (x - x')) y = ↑(↑f x) y - ↑(↑f x') y
[PROOFSTEP]
rw [f.map_sub, sub_apply]
[GOAL]
𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace 𝕜 G
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
x : M
y : F
⊢ ↑(↑f (-x)) y = -↑(↑f x) y
[PROOFSTEP]
rw [f.map_neg, neg_apply]
[GOAL]
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace 𝕜 G
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁴ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜₂ G'
inst✝¹ : NormedSpace 𝕜' G'
inst✝ : SMulCommClass 𝕜₂ 𝕜' G'
f : E →L[𝕜] F →L[𝕜] G
c : 𝕜
x : E
y : F
⊢ ↑(↑f (c • x)) y = c • ↑(↑f x) y
[PROOFSTEP]
rw [f.map_smul, smul_apply]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f✝ : E × F → G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ * ‖x‖ * ‖y‖ ≤ max ‖f‖ 1 * ‖x‖ * ‖y‖
[PROOFSTEP]
apply_rules [mul_le_mul_of_nonneg_right, norm_nonneg, le_max_left]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
Cpos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
x✝ : E × F
x : E
y : F
⊢ ‖f (x, y)‖ ≤ ?m.264130 h C Cpos hC * ‖‖(x, y).fst‖ * ‖(x, y).snd‖‖
[PROOFSTEP]
simpa [mul_assoc] using hC x y
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
⊢ Continuous f
[PROOFSTEP]
refine continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun n => f n - f x) (𝓝 x) (𝓝 0)
[PROOFSTEP]
suffices : Tendsto (λ y : E × F ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0))
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
this : Tendsto (fun y => f (y.fst - x.fst, y.snd) + f (x.fst, y.snd - x.snd)) (𝓝 x) (𝓝 (0 + 0))
⊢ Tendsto (fun n => f n - f x) (𝓝 x) (𝓝 0)
[PROOFSTEP]
simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this
[GOAL]
case this
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun y => f (y.fst - x.fst, y.snd) + f (x.fst, y.snd - x.snd)) (𝓝 x) (𝓝 (0 + 0))
[PROOFSTEP]
apply Tendsto.add
[GOAL]
case this.hf
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun x_1 => f (x_1.fst - x.fst, x_1.snd)) (𝓝 x) (𝓝 0)
[PROOFSTEP]
rw [← isLittleO_one_iff ℝ, ← one_mul 1]
[GOAL]
case this.hf
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ (fun x_1 => f (x_1.fst - x.fst, x_1.snd)) =o[𝓝 x] fun _x => 1 * 1
[PROOFSTEP]
refine h.isBigO_comp.trans_isLittleO ?_
[GOAL]
case this.hf
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ (fun x_1 => ‖x_1.fst - x.fst‖ * ‖x_1.snd‖) =o[𝓝 x] fun _x => 1 * 1
[PROOFSTEP]
refine (IsLittleO.norm_left ?_).mul_isBigO (IsBigO.norm_left ?_)
[GOAL]
case this.hf.refine_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ (fun x_1 => x_1.fst - x.fst) =o[𝓝 x] fun _x => 1
[PROOFSTEP]
exact (isLittleO_one_iff _).2 (tendsto_sub_nhds_zero_iff.2 (continuous_fst.tendsto _))
[GOAL]
case this.hf.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ (fun x => x.snd) =O[𝓝 x] fun _x => 1
[PROOFSTEP]
exact (continuous_snd.tendsto _).isBigO_one ℝ
[GOAL]
case this.hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun x_1 => f (x.fst, x_1.snd - x.snd)) (𝓝 x) (𝓝 0)
[PROOFSTEP]
refine Continuous.tendsto' ?_ _ _ (by rw [h.map_sub_right, sub_self])
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ f (x.fst, x.snd - x.snd) = 0
[PROOFSTEP]
rw [h.map_sub_right, sub_self]
[GOAL]
case this.hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Continuous fun x_1 => f (x.fst, x_1.snd - x.snd)
[PROOFSTEP]
exact ((h.toContinuousLinearMap x.1).continuous).comp (continuous_snd.sub continuous_const)
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
⊢ IsBoundedBilinearMap 𝕜 fun p => p.fst * p.snd
[PROOFSTEP]
simp_rw [← smul_eq_mul]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
⊢ IsBoundedBilinearMap 𝕜 fun p => p.fst • p.snd
[PROOFSTEP]
exact isBoundedBilinearMap_smul
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
⊢ IsOpen (range toContinuousLinearMap)
[PROOFSTEP]
rw [isOpen_iff_mem_nhds, forall_range_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
⊢ ∀ (i : E ≃L[𝕜] F), range toContinuousLinearMap ∈ 𝓝 ↑i
[PROOFSTEP]
refine' fun e => IsOpen.mem_nhds _ (mem_range_self _)
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
⊢ IsOpen (range toContinuousLinearMap)
[PROOFSTEP]
let O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
⊢ IsOpen (range toContinuousLinearMap)
[PROOFSTEP]
have h_O : Continuous O := isBoundedBilinearMap_comp.continuous_right
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
⊢ IsOpen (range toContinuousLinearMap)
[PROOFSTEP]
convert show IsOpen (O ⁻¹' {x | IsUnit x}) from Units.isOpen.preimage h_O using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
⊢ range toContinuousLinearMap = O ⁻¹' {x | IsUnit x}
[PROOFSTEP]
ext f'
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ range toContinuousLinearMap ↔ f' ∈ O ⁻¹' {x | IsUnit x}
[PROOFSTEP]
constructor
[GOAL]
case h.e'_3.h.mp
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ range toContinuousLinearMap → f' ∈ O ⁻¹' {x | IsUnit x}
[PROOFSTEP]
rintro ⟨e', rfl⟩
[GOAL]
case h.e'_3.h.mp.intro
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
e' : E ≃L[𝕜] F
⊢ ↑e' ∈ O ⁻¹' {x | IsUnit x}
[PROOFSTEP]
exact ⟨(e'.trans e.symm).toUnit, rfl⟩
[GOAL]
case h.e'_3.h.mpr
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ O ⁻¹' {x | IsUnit x} → f' ∈ range toContinuousLinearMap
[PROOFSTEP]
rintro ⟨w, hw⟩
[GOAL]
case h.e'_3.h.mpr.intro
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : ↑w = O f'
⊢ f' ∈ range toContinuousLinearMap
[PROOFSTEP]
use(unitsEquiv 𝕜 E w).trans e
[GOAL]
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : ↑w = O f'
⊢ ↑(ContinuousLinearEquiv.trans (↑(unitsEquiv 𝕜 E) w) e) = f'
[PROOFSTEP]
ext x
[GOAL]
case h.h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => comp (↑(ContinuousLinearEquiv.symm e)) f
h_O : Continuous O
f' : E →L[𝕜] F
w : (E →L[𝕜] E)ˣ
hw : ↑w = O f'
x : E
⊢ ↑↑(ContinuousLinearEquiv.trans (↑(unitsEquiv 𝕜 E) w) e) x = ↑f' x
[PROOFSTEP]
simp [hw]
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
⊢ ↑e ∈ range toContinuousLinearMap
[PROOFSTEP]
simp


[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
h : a.toProd = b.toProd
⊢ a = b
[PROOFSTEP]
cases a
[GOAL]
case mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
b : 𝓜(𝕜, A)
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), ↑toProd✝.snd x * y = x * ↑toProd✝.fst y
h : { toProd := toProd✝, central := central✝ }.toProd = b.toProd
⊢ { toProd := toProd✝, central := central✝ } = b
[PROOFSTEP]
cases b
[GOAL]
case mk.mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
toProd✝¹ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝¹ : ∀ (x y : A), ↑toProd✝¹.snd x * y = x * ↑toProd✝¹.fst y
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), ↑toProd✝.snd x * y = x * ↑toProd✝.fst y
h : { toProd := toProd✝¹, central := central✝¹ }.toProd = { toProd := toProd✝, central := central✝ }.toProd
⊢ { toProd := toProd✝¹, central := central✝¹ } = { toProd := toProd✝, central := central✝ }
[PROOFSTEP]
simpa using h
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : (A →L[𝕜] A) × (A →L[𝕜] A)
⊢ x ∈ Set.range toProd → x ∈ {lr | ∀ (x y : A), ↑lr.snd x * y = x * ↑lr.fst y}
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ a.toProd ∈ {lr | ∀ (x y : A), ↑lr.snd x * y = x * ↑lr.fst y}
[PROOFSTEP]
exact a.central
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
x y : A
⊢ ↑(a.snd + b.snd) x * y = x * ↑(a.fst + b.fst) y
[PROOFSTEP]
simp only [ContinuousLinearMap.add_apply, mul_add, add_mul, central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x y : A
⊢ -↑a.snd x * y = x * -↑a.fst y
[PROOFSTEP]
simp only [ContinuousLinearMap.neg_apply, neg_mul, mul_neg, central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
x y : A
⊢ ↑(a.snd - b.snd) x * y = x * ↑(a.fst - b.fst) y
[PROOFSTEP]
simp only [ContinuousLinearMap.sub_apply, _root_.sub_mul, _root_.mul_sub, central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : SMulCommClass 𝕜 A A
inst✝⁶ : IsScalarTower 𝕜 A A
S : Type u_3
inst✝⁵ : Monoid S
inst✝⁴ : DistribMulAction S A
inst✝³ : SMulCommClass 𝕜 S A
inst✝² : ContinuousConstSMul S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass S A A
s : S
a : 𝓜(𝕜, A)
x y : A
⊢ ↑(s • a.snd) x * y = x * ↑(s • a.fst) y
[PROOFSTEP]
simp only [ContinuousLinearMap.smul_apply, mul_smul_comm, smul_mul_assoc, central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
x y : A
⊢ ↑b.snd (↑a.snd x) * y = x * ↑a.fst (↑b.fst y)
[PROOFSTEP]
simp only [central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℕ
x y : A
⊢ ↑(↑n).snd x * y = x * ↑(↑n).fst y
[PROOFSTEP]
rw [Prod.snd_natCast, Prod.fst_natCast]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℕ
x y : A
⊢ ↑↑n x * y = x * ↑↑n y
[PROOFSTEP]
simp only [← Nat.smul_one_eq_coe, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℤ
x y : A
⊢ ↑(↑n).snd x * y = x * ↑(↑n).fst y
[PROOFSTEP]
rw [Prod.snd_intCast, Prod.fst_intCast]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℤ
x y : A
⊢ ↑↑n x * y = x * ↑↑n y
[PROOFSTEP]
simp only [← Int.smul_one_eq_coe, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
n : ℕ
x y : A
⊢ ↑(a.toProd ^ n).snd x * y = x * ↑(a.toProd ^ n).fst y
[PROOFSTEP]
induction' n with k hk generalizing x y
[GOAL]
case zero
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x✝ y✝ x y : A
⊢ ↑(a.toProd ^ Nat.zero).snd x * y = x * ↑(a.toProd ^ Nat.zero).fst y
[PROOFSTEP]
rfl
[GOAL]
case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x✝ y✝ : A
k : ℕ
hk : ∀ (x y : A), ↑(a.toProd ^ k).snd x * y = x * ↑(a.toProd ^ k).fst y
x y : A
⊢ ↑(a.toProd ^ Nat.succ k).snd x * y = x * ↑(a.toProd ^ Nat.succ k).fst y
[PROOFSTEP]
rw [Prod.pow_snd, Prod.pow_fst] at hk ⊢
[GOAL]
case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x✝ y✝ : A
k : ℕ
hk : ∀ (x y : A), ↑(a.snd ^ k) x * y = x * ↑(a.fst ^ k) y
x y : A
⊢ ↑(a.snd ^ Nat.succ k) x * y = x * ↑(a.fst ^ Nat.succ k) y
[PROOFSTEP]
rw [pow_succ a.snd, mul_apply, a.central, hk, pow_succ' a.fst, mul_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ
⊢ x ∈ Set.range toProdMulOpposite → x ∈ {lr | ∀ (x y : A), ↑(unop lr.snd) x * y = x * ↑lr.fst y}
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ toProdMulOpposite a ∈ {lr | ∀ (x y : A), ↑(unop lr.snd) x * y = x * ↑lr.fst y}
[PROOFSTEP]
exact a.central
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
k : 𝕜
x y : A
⊢ ↑(↑(algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k).snd x * y =
    x * ↑(↑(algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k).fst y
[PROOFSTEP]
simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
a : 𝓜(𝕜, A)
x y : A
⊢ ↑(comp (comp (↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)) a.snd)
                ↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv),
              comp (comp (↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)) a.fst)
                ↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)).snd
        x *
      y =
    x *
      ↑(comp (comp (↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)) a.snd)
                ↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv),
              comp (comp (↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)) a.fst)
                ↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)).fst
        y
[PROOFSTEP]
simpa only [star_mul, star_star] using (congr_arg star (a.central (star y) (star x))).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x : 𝓜(𝕜, A)
⊢ star (star x) = x
[PROOFSTEP]
ext
[GOAL]
case h.h₁.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (star x)).fst x✝ = ↑x.fst x✝
[PROOFSTEP]
simp only [star_fst, star_snd, star_star]
[GOAL]
case h.h₂.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (star x)).snd x✝ = ↑x.snd x✝
[PROOFSTEP]
simp only [star_fst, star_snd, star_star]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x y : 𝓜(𝕜, A)
⊢ star (x + y) = star x + star y
[PROOFSTEP]
ext
[GOAL]
case h.h₁.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x y : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (x + y)).fst x✝ = ↑(star x + star y).fst x✝
[PROOFSTEP]
simp only [star_fst, star_snd, add_fst, add_snd, ContinuousLinearMap.add_apply, star_add]
[GOAL]
case h.h₂.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x y : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (x + y)).snd x✝ = ↑(star x + star y).snd x✝
[PROOFSTEP]
simp only [star_fst, star_snd, add_fst, add_snd, ContinuousLinearMap.add_apply, star_add]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
a b : 𝓜(𝕜, A)
⊢ star (a * b) = star b * star a
[PROOFSTEP]
ext
[GOAL]
case h.h₁.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
a b : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (a * b)).fst x✝ = ↑(star b * star a).fst x✝
[PROOFSTEP]
simp only [star_fst, star_snd, mul_fst, mul_snd, star_star, ContinuousLinearMap.coe_mul, Function.comp_apply]
[GOAL]
case h.h₂.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
a b : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (a * b)).snd x✝ = ↑(star b * star a).snd x✝
[PROOFSTEP]
simp only [star_fst, star_snd, mul_fst, mul_snd, star_star, ContinuousLinearMap.coe_mul, Function.comp_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
k : 𝕜
a : 𝓜(𝕜, A)
⊢ star (k • a) = star k • star a
[PROOFSTEP]
ext
[GOAL]
case h.h₁.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
k : 𝕜
a : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (k • a)).fst x✝ = ↑(star k • star a).fst x✝
[PROOFSTEP]
exact star_smul _ _
[GOAL]
case h.h₂.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
k : 𝕜
a : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (k • a)).snd x✝ = ↑(star k • star a).snd x✝
[PROOFSTEP]
exact star_smul _ _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
⊢ ↑𝕜 = ↑(algebraMap 𝕜 𝓜(𝕜, 𝕜))
[PROOFSTEP]
ext x : 3
[GOAL]
case h.h.h₁
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : 𝕜
⊢ (↑𝕜 x).toProd.fst = (↑(algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).fst
[PROOFSTEP]
rfl
  -- `fst` is defeq
[GOAL]
case h.h.h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : 𝕜
⊢ (↑𝕜 x).toProd.snd = (↑(algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).snd
[PROOFSTEP]
refine ContinuousLinearMap.ext fun y => ?_
[GOAL]
case h.h.h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x y : 𝕜
⊢ ↑(↑𝕜 x).toProd.snd y = ↑(↑(algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).snd y
[PROOFSTEP]
exact mul_comm y x
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
⊢ Function.Injective ↑toProdMulOppositeHom
[PROOFSTEP]
simpa using toProdMulOpposite_injective
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ CompleteSpace 𝓜(𝕜, A)
[PROOFSTEP]
rw [completeSpace_iff_isComplete_range uniformEmbedding_toProdMulOpposite.toUniformInducing]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsComplete (Set.range toProdMulOpposite)
[PROOFSTEP]
apply IsClosed.isComplete
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsClosed (Set.range toProdMulOpposite)
[PROOFSTEP]
simp only [range_toProdMulOpposite, Set.setOf_forall]
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsClosed (⋂ (i : A) (i_1 : A), {x | ↑(unop x.snd) i * i_1 = i * ↑x.fst i_1})
[PROOFSTEP]
refine' isClosed_iInter fun x => isClosed_iInter fun y => isClosed_eq _ _
[GOAL]
case h.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
x y : A
⊢ Continuous fun x_1 => ↑(unop x_1.snd) x * y
case h.refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
x y : A
⊢ Continuous fun x_1 => x * ↑x_1.fst y
[PROOFSTEP]
exact ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp <| continuous_unop.comp continuous_snd).mul continuous_const
[GOAL]
case h.refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
x y : A
⊢ Continuous fun x_1 => x * ↑x_1.fst y
[PROOFSTEP]
exact continuous_const.mul ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp continuous_fst)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.fst‖ = ‖a.snd‖
[PROOFSTEP]
have h0 : ∀ f : A →L[𝕜] A, ∀ C : ℝ≥0, (∀ b : A, ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C :=
  by
  intro f C h
  have h1 : ∀ b, C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2 :=
    by
    intro b
    convert mul_le_mul_right' (mul_le_mul_left' (f.le_op_nnnorm b) C) ‖b‖₊ using 1
    ring
  have :=
    NNReal.div_le_of_le_mul
      (f.op_nnnorm_le_bound _
        (by simpa only [sqrt_sq, sqrt_mul] using fun b => sqrt_le_sqrt_iff.mpr ((h b).trans (h1 b))))
  convert NNReal.rpow_le_rpow this two_pos.le
  · simp only [NNReal.rpow_two, div_pow, sq_sqrt]
    simp only [sq, mul_self_div_self]
  · simp only [NNReal.rpow_two, sq_sqrt]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
⊢ ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
[PROOFSTEP]
intro f C h
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
⊢ ‖f‖₊ ≤ C
[PROOFSTEP]
have h1 : ∀ b, C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2 :=
  by
  intro b
  convert mul_le_mul_right' (mul_le_mul_left' (f.le_op_nnnorm b) C) ‖b‖₊ using 1
  ring
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
⊢ ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
[PROOFSTEP]
intro b
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
b : A
⊢ C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
[PROOFSTEP]
convert mul_le_mul_right' (mul_le_mul_left' (f.le_op_nnnorm b) C) ‖b‖₊ using 1
[GOAL]
case h.e'_4
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
b : A
⊢ C * ‖f‖₊ * ‖b‖₊ ^ 2 = C * (‖f‖₊ * ‖b‖₊) * ‖b‖₊
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
⊢ ‖f‖₊ ≤ C
[PROOFSTEP]
have :=
  NNReal.div_le_of_le_mul
    (f.op_nnnorm_le_bound _
      (by simpa only [sqrt_sq, sqrt_mul] using fun b => sqrt_le_sqrt_iff.mpr ((h b).trans (h1 b))))
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
⊢ ∀ (x : A), ‖↑f x‖₊ ≤ ?m.1273079 * ?m.1273080 * ‖x‖₊
[PROOFSTEP]
simpa only [sqrt_sq, sqrt_mul] using fun b => sqrt_le_sqrt_iff.mpr ((h b).trans (h1 b))
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / ↑sqrt ‖f‖₊ ≤ ↑sqrt C
⊢ ‖f‖₊ ≤ C
[PROOFSTEP]
convert NNReal.rpow_le_rpow this two_pos.le
[GOAL]
case h.e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / ↑sqrt ‖f‖₊ ≤ ↑sqrt C
⊢ ‖f‖₊ = (‖f‖₊ / ↑sqrt ‖f‖₊) ^ 2
[PROOFSTEP]
simp only [NNReal.rpow_two, div_pow, sq_sqrt]
[GOAL]
case h.e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / ↑sqrt ‖f‖₊ ≤ ↑sqrt C
⊢ ‖f‖₊ = ‖f‖₊ ^ 2 / ‖f‖₊
[PROOFSTEP]
simp only [sq, mul_self_div_self]
[GOAL]
case h.e'_4
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / ↑sqrt ‖f‖₊ ≤ ↑sqrt C
⊢ C = ↑sqrt C ^ 2
[PROOFSTEP]
simp only [NNReal.rpow_two, sq_sqrt]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
⊢ ‖a.fst‖ = ‖a.snd‖
[PROOFSTEP]
have h1 : ∀ b, ‖a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ :=
  by
  intro b
  calc
    ‖a.fst b‖₊ ^ 2 = ‖star (a.fst b) * a.fst b‖₊ := by simpa only [← sq] using CstarRing.nnnorm_star_mul_self.symm
    _ ≤ ‖a.snd (star (a.fst b))‖₊ * ‖b‖₊ := (a.central (star (a.fst b)) b ▸ nnnorm_mul_le _ _)
    _ ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ := nnnorm_star (a.fst b) ▸ mul_le_mul_right' (a.snd.le_op_nnnorm _) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
⊢ ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
[PROOFSTEP]
intro b
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
b : A
⊢ ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
[PROOFSTEP]
calc
  ‖a.fst b‖₊ ^ 2 = ‖star (a.fst b) * a.fst b‖₊ := by simpa only [← sq] using CstarRing.nnnorm_star_mul_self.symm
  _ ≤ ‖a.snd (star (a.fst b))‖₊ * ‖b‖₊ := (a.central (star (a.fst b)) b ▸ nnnorm_mul_le _ _)
  _ ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ := nnnorm_star (a.fst b) ▸ mul_le_mul_right' (a.snd.le_op_nnnorm _) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
b : A
⊢ ‖↑a.fst b‖₊ ^ 2 = ‖star (↑a.fst b) * ↑a.fst b‖₊
[PROOFSTEP]
simpa only [← sq] using CstarRing.nnnorm_star_mul_self.symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
⊢ ‖a.fst‖ = ‖a.snd‖
[PROOFSTEP]
have h2 : ∀ b, ‖a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ :=
  by
  intro b
  calc
    ‖a.snd b‖₊ ^ 2 = ‖a.snd b * star (a.snd b)‖₊ := by simpa only [← sq] using CstarRing.nnnorm_self_mul_star.symm
    _ ≤ ‖b‖₊ * ‖a.fst (star (a.snd b))‖₊ := ((a.central b (star (a.snd b))).symm ▸ nnnorm_mul_le _ _)
    _ = ‖a.fst (star (a.snd b))‖₊ * ‖b‖₊ := (mul_comm _ _)
    _ ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ := nnnorm_star (a.snd b) ▸ mul_le_mul_right' (a.fst.le_op_nnnorm _) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
⊢ ∀ (b : A), ‖↑a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖↑a.snd b‖₊ * ‖b‖₊
[PROOFSTEP]
intro b
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
b : A
⊢ ‖↑a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖↑a.snd b‖₊ * ‖b‖₊
[PROOFSTEP]
calc
  ‖a.snd b‖₊ ^ 2 = ‖a.snd b * star (a.snd b)‖₊ := by simpa only [← sq] using CstarRing.nnnorm_self_mul_star.symm
  _ ≤ ‖b‖₊ * ‖a.fst (star (a.snd b))‖₊ := ((a.central b (star (a.snd b))).symm ▸ nnnorm_mul_le _ _)
  _ = ‖a.fst (star (a.snd b))‖₊ * ‖b‖₊ := (mul_comm _ _)
  _ ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ := nnnorm_star (a.snd b) ▸ mul_le_mul_right' (a.fst.le_op_nnnorm _) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
b : A
⊢ ‖↑a.snd b‖₊ ^ 2 = ‖↑a.snd b * star (↑a.snd b)‖₊
[PROOFSTEP]
simpa only [← sq] using CstarRing.nnnorm_self_mul_star.symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
h2 : ∀ (b : A), ‖↑a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖↑a.snd b‖₊ * ‖b‖₊
⊢ ‖a.fst‖ = ‖a.snd‖
[PROOFSTEP]
exact le_antisymm (h0 _ _ h1) (h0 _ _ h2)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.fst‖ = ‖a‖
[PROOFSTEP]
simp only [norm_def, toProdHom_apply, Prod.norm_def, norm_fst_eq_snd, max_eq_right le_rfl]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.snd‖ = ‖a‖
[PROOFSTEP]
rw [← norm_fst, norm_fst_eq_snd]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
have hball : (Metric.closedBall (0 : A) 1).Nonempty := Metric.nonempty_closedBall.2 zero_le_one
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
have key : ∀ x y, ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.snd (star (a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊ :=
  by
  intro x y hx hy
  rw [a.central]
  calc
    ‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
      nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
    _ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
      (mul_le_mul' (a.fst.le_op_norm_of_le ((nnnorm_star x).trans_le hx)) (a.fst.le_op_norm_of_le hy))
    _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
⊢ ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
intro x y hx hy
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
rw [a.central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖star (↑a.fst (star x)) * ↑a.fst y‖₊ ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
calc
  ‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
    nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
  _ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
    (mul_le_mul' (a.fst.le_op_norm_of_le ((nnnorm_star x).trans_le hx)) (a.fst.le_op_norm_of_le hy))
  _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simp only [mul_one, nnnorm_fst, le_rfl]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
rw [← nnnorm_snd]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ ‖(star a * a).snd‖₊ = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simp only [mul_snd, ← sSup_closed_unit_ball_eq_nnnorm, star_snd, mul_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ sSup ((fun a_1 => ‖↑a.snd (star (↑a.fst (star a_1)))‖₊) '' Metric.closedBall 0 1) = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simp only [← @_root_.op_nnnorm_mul 𝕜 A]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ sSup ((fun a_1 => ‖↑(ContinuousLinearMap.mul 𝕜 A) (↑a.snd (star (↑a.fst (star a_1))))‖₊) '' Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simp only [← sSup_closed_unit_ball_eq_nnnorm, mul_apply']
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun a_1 => sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
refine' csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) _ fun r hr => _
[GOAL]
case refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ ∀ (a_1 : ℝ≥0),
    a_1 ∈
        (fun a_2 => sSup ((fun a_3 => ‖↑a.snd (star (↑a.fst (star a_2))) * a_3‖₊) '' Metric.closedBall 0 1)) ''
          Metric.closedBall 0 1 →
      a_1 ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
rintro - ⟨x, hx, rfl⟩
[GOAL]
case refine'_1.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
x : A
hx : x ∈ Metric.closedBall 0 1
⊢ (fun a_1 => sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)) x ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
refine' csSup_le (hball.image _) _
[GOAL]
case refine'_1.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
x : A
hx : x ∈ Metric.closedBall 0 1
⊢ ∀ (b : ℝ≥0), b ∈ (fun a_1 => ‖↑a.snd (star (↑a.fst (star x))) * a_1‖₊) '' Metric.closedBall 0 1 → b ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
rintro - ⟨y, hy, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
x : A
hx : x ∈ Metric.closedBall 0 1
y : A
hy : y ∈ Metric.closedBall 0 1
⊢ (fun a_1 => ‖↑a.snd (star (↑a.fst (star x))) * a_1‖₊) y ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
exact key x y (mem_closedBall_zero_iff.1 hx) (mem_closedBall_zero_iff.1 hy)
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
⊢ ∃ a_1,
    a_1 ∈
        (fun a_2 => sSup ((fun a_3 => ‖↑a.snd (star (↑a.fst (star a_2))) * a_3‖₊) '' Metric.closedBall 0 1)) ''
          Metric.closedBall 0 1 ∧
      r < a_1
[PROOFSTEP]
simp only [Set.mem_image, Set.mem_setOf_eq, exists_prop, exists_exists_and_eq_and]
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
have hr' : NNReal.sqrt r < ‖a‖₊ := ‖a‖₊.sqrt_mul_self ▸ NNReal.sqrt_lt_sqrt_iff.2 hr
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < ‖a‖₊
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
simp_rw [← nnnorm_fst, ← sSup_closed_unit_ball_eq_nnnorm] at hr'
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
obtain ⟨_, ⟨x, hx, rfl⟩, hxr⟩ := exists_lt_of_lt_csSup (hball.image _) hr'
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
have hx' : ‖x‖₊ ≤ 1 := mem_closedBall_zero_iff.1 hx
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
refine' ⟨star x, mem_closedBall_zero_iff.2 ((nnnorm_star x).trans_le hx'), _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ r < sSup ((fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
refine' lt_csSup_of_lt _ ⟨x, hx, rfl⟩ _
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ BddAbove ((fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
refine' ⟨‖a‖₊ * ‖a‖₊, _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ ‖a‖₊ * ‖a‖₊ ∈ upperBounds ((fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
rintro - ⟨y, hy, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_1.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
y : A
hy : y ∈ Metric.closedBall 0 1
⊢ (fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) y ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
exact key (star x) y ((nnnorm_star x).trans_le hx') (mem_closedBall_zero_iff.1 hy)
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ r < (fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) x
[PROOFSTEP]
simpa only [a.central, star_star, CstarRing.nnnorm_star_mul_self, NNReal.sq_sqrt, ← sq] using
  pow_lt_pow_of_lt_left hxr zero_le' two_pos