Theorem shsel

Description: Membership in the subspace sum of two Hilbert subspaces. (Contributed by NM, 14-Dec-2004) (Revised by Mario Carneiro, 29-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	shsel	|- ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x +h y ) ) )

Proof

Step	Hyp	Ref	Expression
1		shsval	|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( +h " ( A X. B ) ) )
2	1	eleq2d	|- ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> C e. ( +h " ( A X. B ) ) ) )
3		ax-hfvadd	|- +h : ( ~H X. ~H ) --> ~H
4		ffn	|- ( +h : ( ~H X. ~H ) --> ~H -> +h Fn ( ~H X. ~H ) )
5	3 4	ax-mp	|- +h Fn ( ~H X. ~H )
6		shss	|- ( A e. SH -> A C_ ~H )
7		shss	|- ( B e. SH -> B C_ ~H )
8		xpss12	|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A X. B ) C_ ( ~H X. ~H ) )
9	6 7 8	syl2an	|- ( ( A e. SH /\ B e. SH ) -> ( A X. B ) C_ ( ~H X. ~H ) )
10		ovelimab	|- ( ( +h Fn ( ~H X. ~H ) /\ ( A X. B ) C_ ( ~H X. ~H ) ) -> ( C e. ( +h " ( A X. B ) ) <-> E. x e. A E. y e. B C = ( x +h y ) ) )
11	5 9 10	sylancr	|- ( ( A e. SH /\ B e. SH ) -> ( C e. ( +h " ( A X. B ) ) <-> E. x e. A E. y e. B C = ( x +h y ) ) )
12	2 11	bitrd	|- ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x +h y ) ) )