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