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