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