Metamath Proof Explorer


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 ) ) )