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)ᗮ
h : v +ᵥ p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑(orthogonalProjection s) (v +ᵥ p) = { val := p, property := hp }
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)ᗮ
⊢ ↑(orthogonalProjection s) (v +ᵥ p) = { val := p, property := hp }
have h := vsub_orthogonalProjection_mem_direction_orthogonal s (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)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑(orthogonalProjection s) (v +ᵥ p) = { val := p, property := hp }
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)ᗮ
h : v +ᵥ p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑(orthogonalProjection s) (v +ᵥ p) = { val := p, property := hp }
rw [vadd_vsub_assoc, Submodule.add_mem_iff_right _ hv] at h
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)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ { val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p) = 0
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)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑(orthogonalProjection s) (v +ᵥ p) = { val := p, property := hp }
refine' (eq_of_vsub_eq_zero _).symm
case a
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)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑({ val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p)) = ↑0
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)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ { val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p) = 0
ext
case a
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)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑({ val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p)) ∈ direction s
case a
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)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑({ val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p)) = ↑0
refine' Submodule.disjoint_def.1 s.direction.orthogonal_disjoint _ _ h
no goals
case a
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)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑({ val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p)) ∈ direction s
exact (_ : s.direction).2