This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐻 ∈ Cℋ → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) = ℋ )

Proof

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