English
For a linear isometry f with f 1 = 1, for every z, (f z).im is either Im(z) or -Im(z).
Русский
Для линейной изометрии f с f 1 = 1, для всех z, (f z).im равно либо Im(z), либо -Im(z).
LaTeX
$$$\forall {f : ℂ \toℓᵢ[ℝ] ℂ}, (f 1 = 1) \rightarrow \forall z, (f z).im = z.im \lor (f z).im = - z.im$$$
Lean4
theorem im_apply_eq_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : z + conj z = f z + conj (f z) :=
by
have : ‖f z - 1‖ = ‖z - 1‖ := by rw [← f.norm_map (z - 1), f.map_sub, h]
apply_fun fun x => x ^ 2 at this
simp only [← normSq_eq_norm_sq] at this
rw [← ofReal_inj, ← mul_conj, ← mul_conj] at this
rw [RingHom.map_sub, RingHom.map_sub] at this
simp only [sub_mul, mul_sub, one_mul] at this
rw [mul_conj, normSq_eq_norm_sq, LinearIsometry.norm_map] at this
rw [mul_conj, normSq_eq_norm_sq] at this
simp only [sub_sub, sub_right_inj, mul_one, ofReal_pow, RingHom.map_one] at this
simp only [add_sub, sub_left_inj] at this
rw [add_comm, ← this, add_comm]
