Metamath Proof Explorer


Theorem shsva

Description: Vector sum belongs to subspace sum. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion shsva
|- ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( C +h D ) e. ( A +H B ) ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( C +h D ) = ( C +h D )
2 rspceov
 |-  ( ( C e. A /\ D e. B /\ ( C +h D ) = ( C +h D ) ) -> E. x e. A E. y e. B ( C +h D ) = ( x +h y ) )
3 1 2 mp3an3
 |-  ( ( C e. A /\ D e. B ) -> E. x e. A E. y e. B ( C +h D ) = ( x +h y ) )
4 shsel
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( C +h D ) e. ( A +H B ) <-> E. x e. A E. y e. B ( C +h D ) = ( x +h y ) ) )
5 3 4 syl5ibr
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( C +h D ) e. ( A +H B ) ) )