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ℋ ∧ 𝐴 ∈ ℋ ) → ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )