[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ Submodule.span ℝ ↑{1, I} = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ⊤ ≤ Submodule.span ℝ ↑{1, I}
[PROOFSTEP]
intro a _
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ a ∈ Submodule.span ℝ ↑{1, I}
[PROOFSTEP]
rw [Finset.coe_insert, Finset.coe_singleton, Submodule.mem_span_insert]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ ∃ a_1 z, z ∈ Submodule.span ℝ {I} ∧ a = a_1 • 1 + z
[PROOFSTEP]
refine' ⟨re a, im a • I, _, _⟩
[GOAL]
case refine'_1
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ ↑im a • I ∈ Submodule.span ℝ {I}
[PROOFSTEP]
rw [Submodule.mem_span_singleton]
[GOAL]
case refine'_1
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ ∃ a_1, a_1 • I = ↑im a • I
[PROOFSTEP]
use im a
[GOAL]
case refine'_2
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ a = ↑re a • 1 + ↑im a • I
[PROOFSTEP]
simp [re_add_im a, Algebra.smul_def, algebraMap_eq_ofReal]
[GOAL]
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
⊢ ProperSpace E
[PROOFSTEP]
letI : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
[GOAL]
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
⊢ ProperSpace E
[PROOFSTEP]
letI : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E
[GOAL]
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this✝ : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
this : FiniteDimensional ℝ E := trans ℝ K E
⊢ ProperSpace E
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ‖reClm‖ = 1
[PROOFSTEP]
apply le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ 1 ≤ ‖LinearMap.mkContinuous reLm 1 (_ : ∀ (x : K), ‖↑reLm x‖ ≤ 1 * ‖x‖)‖
[PROOFSTEP]
convert ContinuousLinearMap.ratio_le_op_norm (reClm : K →L[ℝ] ℝ) (1 : K)
[GOAL]
case h.e'_3
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ 1 = ‖↑reClm 1‖ / ‖1‖
[PROOFSTEP]
simp
