Metamath Proof Explorer

Theorem pjhth

Description: Projection Theorem: Any Hilbert space vector A can be decomposed uniquely into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of Beran p. 102 (existence part). (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjhth ⊢ H ∈ C ℋ → H + ℋ ⊥ ⁡ H = ℋ

Proof

Step Hyp Ref Expression
1 chsh ⊢ H ∈ C ℋ → H ∈ S ℋ
2 shocsh ⊢ H ∈ S ℋ → ⊥ ⁡ H ∈ S ℋ
3 shsss ⊢ H ∈ S ℋ ∧ ⊥ ⁡ H ∈ S ℋ → H + ℋ ⊥ ⁡ H ⊆ ℋ
4 1 2 3 syl2anc2 ⊢ H ∈ C ℋ → H + ℋ ⊥ ⁡ H ⊆ ℋ
5 fveq2 ⊢ H = if H ∈ C ℋ H ℋ → ⊥ ⁡ H = ⊥ ⁡ if H ∈ C ℋ H ℋ
6 5 rexeqdv ⊢ H = if H ∈ C ℋ H ℋ → ∃ z ∈ ⊥ ⁡ H x = y + ℎ z ↔ ∃ z ∈ ⊥ ⁡ if H ∈ C ℋ H ℋ x = y + ℎ z
7 6 rexeqbi1dv ⊢ H = if H ∈ C ℋ H ℋ → ∃ y ∈ H ∃ z ∈ ⊥ ⁡ H x = y + ℎ z ↔ ∃ y ∈ if H ∈ C ℋ H ℋ ∃ z ∈ ⊥ ⁡ if H ∈ C ℋ H ℋ x = y + ℎ z
8 7 imbi2d ⊢ H = if H ∈ C ℋ H ℋ → x ∈ ℋ → ∃ y ∈ H ∃ z ∈ ⊥ ⁡ H x = y + ℎ z ↔ x ∈ ℋ → ∃ y ∈ if H ∈ C ℋ H ℋ ∃ z ∈ ⊥ ⁡ if H ∈ C ℋ H ℋ x = y + ℎ z
9 ifchhv ⊢ if H ∈ C ℋ H ℋ ∈ C ℋ
10 id ⊢ x ∈ ℋ → x ∈ ℋ
11 9 10 pjhthlem2 ⊢ x ∈ ℋ → ∃ y ∈ if H ∈ C ℋ H ℋ ∃ z ∈ ⊥ ⁡ if H ∈ C ℋ H ℋ x = y + ℎ z
12 8 11 dedth ⊢ H ∈ C ℋ → x ∈ ℋ → ∃ y ∈ H ∃ z ∈ ⊥ ⁡ H x = y + ℎ z
13 shsel ⊢ H ∈ S ℋ ∧ ⊥ ⁡ H ∈ S ℋ → x ∈ H + ℋ ⊥ ⁡ H ↔ ∃ y ∈ H ∃ z ∈ ⊥ ⁡ H x = y + ℎ z
14 1 2 13 syl2anc2 ⊢ H ∈ C ℋ → x ∈ H + ℋ ⊥ ⁡ H ↔ ∃ y ∈ H ∃ z ∈ ⊥ ⁡ H x = y + ℎ z
15 12 14 sylibrd ⊢ H ∈ C ℋ → x ∈ ℋ → x ∈ H + ℋ ⊥ ⁡ H
16 15 ssrdv ⊢ H ∈ C ℋ → ℋ ⊆ H + ℋ ⊥ ⁡ H
17 4 16 eqssd ⊢ H ∈ C ℋ → H + ℋ ⊥ ⁡ H = ℋ