This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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