[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
let fc : F → 𝕜 := fun x => (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x)
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have add : ∀ x y : F, fc (x + y) = fc x + fc y := by
  intro x y
  simp only [smul_add, LinearMap.map_add, ofReal_add]
  rw [mul_add]
  abel
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
⊢ ∀ (x y : F), fc (x + y) = fc x + fc y
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
x y : F
⊢ fc (x + y) = fc x + fc y
[PROOFSTEP]
simp only [smul_add, LinearMap.map_add, ofReal_add]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
x y : F
⊢ ↑(↑fr x) + ↑(↑fr y) - I * (↑(↑fr (I • x)) + ↑(↑fr (I • y))) =
    ↑(↑fr x) - I * ↑(↑fr (I • x)) + (↑(↑fr y) - I * ↑(↑fr (I • y)))
[PROOFSTEP]
rw [mul_add]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
x y : F
⊢ ↑(↑fr x) + ↑(↑fr y) - (I * ↑(↑fr (I • x)) + I * ↑(↑fr (I • y))) =
    ↑(↑fr x) - I * ↑(↑fr (I • x)) + (↑(↑fr y) - I * ↑(↑fr (I • y)))
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
x y : F
⊢ ↑(↑fr x) + ↑(↑fr y) - (I * ↑(↑fr (I • x)) + I * ↑(↑fr (I • y))) =
    ↑(↑fr x) - I * ↑(↑fr (I • x)) + (↑(↑fr y) - I * ↑(↑fr (I • y)))
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have A : ∀ (c : ℝ) (x : F), (fr ((c : 𝕜) • x) : 𝕜) = (c : 𝕜) * (fr x : 𝕜) :=
  by
  intro c x
  rw [← ofReal_mul]
  congr 1
  rw [IsROrC.ofReal_alg, smul_assoc, fr.map_smul, Algebra.id.smul_eq_mul, one_smul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
⊢ ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
[PROOFSTEP]
intro c x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
c : ℝ
x : F
⊢ ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
[PROOFSTEP]
rw [← ofReal_mul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
c : ℝ
x : F
⊢ ↑(↑fr (↑c • x)) = ↑(c * ↑fr x)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
c : ℝ
x : F
⊢ ↑fr (↑c • x) = c * ↑fr x
[PROOFSTEP]
rw [IsROrC.ofReal_alg, smul_assoc, fr.map_smul, Algebra.id.smul_eq_mul, one_smul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have smul_ℝ : ∀ (c : ℝ) (x : F), fc ((c : 𝕜) • x) = (c : 𝕜) * fc x :=
  by
  intro c x
  dsimp only
  rw [A c x, smul_smul, mul_comm I (c : 𝕜), ← smul_smul, A, mul_sub]
  ring
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
⊢ ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
[PROOFSTEP]
intro c x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
c : ℝ
x : F
⊢ fc (↑c • x) = ↑c * fc x
[PROOFSTEP]
dsimp only
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
c : ℝ
x : F
⊢ ↑(↑fr (↑c • x)) - I * ↑(↑fr (I • ↑c • x)) = ↑c * (↑(↑fr x) - I * ↑(↑fr (I • x)))
[PROOFSTEP]
rw [A c x, smul_smul, mul_comm I (c : 𝕜), ← smul_smul, A, mul_sub]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
c : ℝ
x : F
⊢ ↑c * ↑(↑fr x) - I * (↑c * ↑(↑fr (I • x))) = ↑c * ↑(↑fr x) - ↑c * (I * ↑(↑fr (I • x)))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have smul_I : ∀ x : F, fc ((I : 𝕜) • x) = (I : 𝕜) * fc x :=
  by
  intro x
  dsimp only
  cases' @I_mul_I_ax 𝕜 _ with h h
  · simp [h]
  rw [mul_sub, ← mul_assoc, smul_smul, h]
  simp only [neg_mul, LinearMap.map_neg, one_mul, one_smul, mul_neg, ofReal_neg, neg_smul, sub_neg_eq_add, add_comm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
⊢ ∀ (x : F), fc (I • x) = I * fc x
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
⊢ fc (I • x) = I * fc x
[PROOFSTEP]
dsimp only
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
⊢ ↑(↑fr (I • x)) - I * ↑(↑fr (I • I • x)) = I * (↑(↑fr x) - I * ↑(↑fr (I • x)))
[PROOFSTEP]
cases' @I_mul_I_ax 𝕜 _ with h h
[GOAL]
case inl
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
h : I = 0
⊢ ↑(↑fr (I • x)) - I * ↑(↑fr (I • I • x)) = I * (↑(↑fr x) - I * ↑(↑fr (I • x)))
[PROOFSTEP]
simp [h]
[GOAL]
case inr
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
h : I * I = -1
⊢ ↑(↑fr (I • x)) - I * ↑(↑fr (I • I • x)) = I * (↑(↑fr x) - I * ↑(↑fr (I • x)))
[PROOFSTEP]
rw [mul_sub, ← mul_assoc, smul_smul, h]
[GOAL]
case inr
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
h : I * I = -1
⊢ ↑(↑fr (I • x)) - I * ↑(↑fr (-1 • x)) = I * ↑(↑fr x) - -1 * ↑(↑fr (I • x))
[PROOFSTEP]
simp only [neg_mul, LinearMap.map_neg, one_mul, one_smul, mul_neg, ofReal_neg, neg_smul, sub_neg_eq_add, add_comm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
have smul_𝕜 : ∀ (c : 𝕜) (x : F), fc (c • x) = c • fc x :=
  by
  intro c x
  rw [← re_add_im c, add_smul, add_smul, add, smul_ℝ, ← smul_smul, smul_ℝ, smul_I, ← mul_assoc]
  rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
⊢ ∀ (c : 𝕜) (x : F), fc (c • x) = c • fc x
[PROOFSTEP]
intro c x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
c : 𝕜
x : F
⊢ fc (c • x) = c • fc x
[PROOFSTEP]
rw [← re_add_im c, add_smul, add_smul, add, smul_ℝ, ← smul_smul, smul_ℝ, smul_I, ← mul_assoc]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
c : 𝕜
x : F
⊢ ↑(↑re c) * fc x + ↑(↑im c) * I * fc x = ↑(↑re c) • fc x + (↑(↑im c) * I) • fc x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
fc : F → 𝕜 := fun x => ↑(↑fr x) - I * ↑(↑fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(↑fr (↑c • x)) = ↑c * ↑(↑fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
smul_𝕜 : ∀ (c : 𝕜) (x : F), fc (c • x) = c • fc x
⊢ F →ₗ[𝕜] 𝕜
[PROOFSTEP]
exact
  { toFun := fc
    map_add' := add
    map_smul' := smul_𝕜 }
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ↑re (↑(extendTo𝕜' fr) x) = ↑fr x
[PROOFSTEP]
simp only [extendTo𝕜'_apply, map_sub, zero_mul, mul_zero, sub_zero, isROrC_simps]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ‖↑(extendTo𝕜' fr) x‖ ^ 2 = ↑re (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) * ↑(extendTo𝕜' fr) x)
[PROOFSTEP]
rw [IsROrC.conj_mul, normSq_eq_def', ofReal_re]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ↑re (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) * ↑(extendTo𝕜' fr) x) =
    ↑fr (↑(starRingEnd ((fun x => 𝕜) x)) (↑(extendTo𝕜' fr) x) • x)
[PROOFSTEP]
rw [← smul_eq_mul, ← map_smul, extendTo𝕜'_apply_re]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
⊢ ‖↑(LinearMap.extendTo𝕜' ↑fr) x‖ ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
set lm : F →ₗ[𝕜] 𝕜 := fr.toLinearMap.extendTo𝕜'
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
by_cases h : lm x = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
rw [h, norm_zero]
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ 0 ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case pos.ha
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ 0 ≤ ‖fr‖
[PROOFSTEP]
exact norm_nonneg _
[GOAL]
case pos.hb
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ 0 ≤ ‖x‖
[PROOFSTEP]
exact norm_nonneg _
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
[PROOFSTEP]
rw [← mul_le_mul_left (norm_pos_iff.2 h), ← sq]
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖↑lm x‖ ^ 2 ≤ ‖↑lm x‖ * (‖fr‖ * ‖x‖)
[PROOFSTEP]
calc
  ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) := fr.toLinearMap.norm_extendTo𝕜'_apply_sq x
  _ ≤ ‖fr (conj (lm x : 𝕜) • x)‖ := (le_abs_self _)
  _ ≤ ‖fr‖ * ‖conj (lm x : 𝕜) • x‖ := (le_op_norm _ _)
  _ = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) := by rw [norm_smul, norm_conj, mul_left_comm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖fr‖ * ‖↑(starRingEnd ((fun x => 𝕜) x)) (↑lm x) • x‖ = ‖↑lm x‖ * (‖fr‖ * ‖x‖)
[PROOFSTEP]
rw [norm_smul, norm_conj, mul_left_comm]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ NormedSpace 𝕜 (RestrictScalars ℝ 𝕜 F)
[PROOFSTEP]
unfold RestrictScalars
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ NormedSpace 𝕜 F
[PROOFSTEP]
infer_instance
