Metamath Proof Explorer


Theorem pjpjhthi

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
Hypotheses pjpjhth.1 A
pjpjhth.2 H C
Assertion pjpjhthi x H y H A = x + y

Proof

Step Hyp Ref Expression
1 pjpjhth.1 A
2 pjpjhth.2 H C
3 pjpjhth H C A x H y H A = x + y
4 2 1 3 mp2an x H y H A = x + y