Theorem pjhtheu

Description: Projection Theorem: Any Hilbert space vector A can be decomposed uniquely 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. See pjhtheu2 for the uniqueness of y . (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	pjhtheu	|- ( ( H e. CH /\ A e. ~H ) -> E! x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )

Proof

Step	Hyp	Ref	Expression
1		pjhth	|- ( H e. CH -> ( H +H ( _|_ ` H ) ) = ~H )
2	1	eleq2d	|- ( H e. CH -> ( A e. ( H +H ( _|_ ` H ) ) <-> A e. ~H ) )
3		chsh	|- ( H e. CH -> H e. SH )
4		shocsh	|- ( H e. SH -> ( _|_ ` H ) e. SH )
5		shsel	|- ( ( H e. SH /\ ( _|_ ` H ) e. SH ) -> ( A e. ( H +H ( _|_ ` H ) ) <-> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
6	3 4 5	syl2anc2	|- ( H e. CH -> ( A e. ( H +H ( _|_ ` H ) ) <-> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
7	2 6	bitr3d	|- ( H e. CH -> ( A e. ~H <-> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
8	7	biimpa	|- ( ( H e. CH /\ A e. ~H ) -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )
9	3 4	syl	|- ( H e. CH -> ( _|_ ` H ) e. SH )
10		ocin	|- ( H e. SH -> ( H i^i ( _|_ ` H ) ) = 0H )
11	3 10	syl	|- ( H e. CH -> ( H i^i ( _|_ ` H ) ) = 0H )
12		pjhthmo	|- ( ( H e. SH /\ ( _|_ ` H ) e. SH /\ ( H i^i ( _|_ ` H ) ) = 0H ) -> E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
13	3 9 11 12	syl3anc	|- ( H e. CH -> E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
14	13	adantr	|- ( ( H e. CH /\ A e. ~H ) -> E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
15		reu5	|- ( E! x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) <-> ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) /\ E* x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
16		df-rmo	|- ( E* x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) <-> E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
17	16	anbi2i	|- ( ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) /\ E* x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) <-> ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) /\ E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) ) )
18	15 17	bitri	|- ( E! x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) <-> ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) /\ E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) ) )
19	8 14 18	sylanbrc	|- ( ( H e. CH /\ A e. ~H ) -> E! x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )