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 H C A x H y H A = x + y

Proof

Step Hyp Ref Expression
1 axpjcl H C A proj H A H
2 choccl H C H C
3 axpjcl H C A proj H A H
4 2 3 sylan H C A proj H A H
5 axpjpj H C A A = proj H A + proj H A
6 rspceov proj H A H proj H A H A = proj H A + proj H A x H y H A = x + y
7 1 4 5 6 syl3anc H C A x H y H A = x + y