𝕜 : Type u_2
E : Type u_1
F : Type ?u.708393
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
⊢ 2 • ↑(↑(orthogonalProjection K) x) = 2 • x ↔ ↑(↑(orthogonalProjection K) x) = x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.708393
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
⊢ ↑(reflection K) x = x ↔ x ∈ K
rw [← orthogonalProjection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,
  two_smul ℕ, ← two_smul 𝕜]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.708393
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
⊢ 2 ≠ 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.708393
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
⊢ 2 • ↑(↑(orthogonalProjection K) x) = 2 • x ↔ ↑(↑(orthogonalProjection K) x) = x
refine' (smul_right_injective E _).eq_iff
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.708393
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
x : E
⊢ 2 ≠ 0
exact two_ne_zero