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 e. ~H
	pjpjhth.2	|- H e. CH
Assertion	pjpjhthi	|- E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y )

Proof

Step	Hyp	Ref	Expression
1		pjpjhth.1	|- A e. ~H
2		pjpjhth.2	|- H e. CH
3		pjpjhth	|- ( ( H e. CH /\ A e. ~H ) -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )
4	2 1 3	mp2an	|- E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y )