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\in \mathscr{H}$$
	pjpjhth.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjpjhthi	$$⊢\exists x\in H\exists y\in \perp \left(H\right)A=x{+}_{ℎ}y$$

Proof

Step	Hyp	Ref	Expression
1		pjpjhth.1	$$⊢A\in \mathscr{H}$$
2		pjpjhth.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjpjhth	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \exists x\in H\exists y\in \perp \left(H\right)A=x{+}_{ℎ}y$$
4	2 1 3	mp2an	$$⊢\exists x\in H\exists y\in \perp \left(H\right)A=x{+}_{ℎ}y$$