V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
⊢ ↑{ val := p, property := hp } -ᵥ p - v +ᵥ ↑{ val := p, property := hp } = -v +ᵥ p
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
⊢ ↑(reflection s) (v +ᵥ p) = -v +ᵥ p
rw [reflection_apply, orthogonalProjection_vadd_eq_self hp hv, vsub_vadd_eq_vsub_sub]
no goals
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
⊢ ↑{ val := p, property := hp } -ᵥ p - v +ᵥ ↑{ val := p, property := hp } = -v +ᵥ p
simp