Metamath Proof Explorer


Theorem pjpjhth

Description: Projection Theorem: Any Hilbert space vector A can be decomposed 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, 6-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion pjpjhth ( ( 𝐻C𝐴 ∈ ℋ ) → ∃ 𝑥𝐻𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 + 𝑦 ) )

Proof

Step Hyp Ref Expression
1 axpjcl ( ( 𝐻C𝐴 ∈ ℋ ) → ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐻 )
2 choccl ( 𝐻C → ( ⊥ ‘ 𝐻 ) ∈ C )
3 axpjcl ( ( ( ⊥ ‘ 𝐻 ) ∈ C𝐴 ∈ ℋ ) → ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) )
4 2 3 sylan ( ( 𝐻C𝐴 ∈ ℋ ) → ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) )
5 axpjpj ( ( 𝐻C𝐴 ∈ ℋ ) → 𝐴 = ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )
6 rspceov ( ( ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ∧ ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐴 = ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) → ∃ 𝑥𝐻𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 + 𝑦 ) )
7 1 4 5 6 syl3anc ( ( 𝐻C𝐴 ∈ ℋ ) → ∃ 𝑥𝐻𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 + 𝑦 ) )