Metamath Proof Explorer

Theorem pjhtheu

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. See pjhtheu2 for the uniqueness of y . (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjhtheu ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ∃! 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 pjhth ⊢ ( 𝐻 ∈ Cℋ → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) = ℋ )
2 1 eleq2d ⊢ ( 𝐻 ∈ Cℋ → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ 𝐴 ∈ ℋ ) )
3 chsh ⊢ ( 𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )
4 shocsh ⊢ ( 𝐻 ∈ Sℋ → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
5 shsel ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( ⊥ ‘ 𝐻 ) ∈ Sℋ ) → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
6 3 4 5 syl2anc2 ⊢ ( 𝐻 ∈ Cℋ → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
7 2 6 bitr3d ⊢ ( 𝐻 ∈ Cℋ → ( 𝐴 ∈ ℋ ↔ ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
8 7 biimpa ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )
9 3 4 syl ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
10 ocin ⊢ ( 𝐻 ∈ Sℋ → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ )
11 3 10 syl ⊢ ( 𝐻 ∈ Cℋ → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ )
12 pjhthmo ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( ⊥ ‘ 𝐻 ) ∈ Sℋ ∧ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ ) → ∃* 𝑥 ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
13 3 9 11 12 syl3anc ⊢ ( 𝐻 ∈ Cℋ → ∃* 𝑥 ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
14 13 adantr ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ∃* 𝑥 ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
15 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ↔ ( ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃* 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
16 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
17 16 anbi2i ⊢ ( ( ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃* 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ↔ ( ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) )
18 15 17 bitri ⊢ ( ∃! 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ↔ ( ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) )
19 8 14 18 sylanbrc ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ∃! 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )