Theorem shsvs

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

	Ref	Expression
Assertion	shsvs	|- ( ( 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		shscl	|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) e. SH )
2	1	a1d	|- ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( A +H B ) e. SH ) )
3		shsel1	|- ( ( A e. SH /\ B e. SH ) -> ( C e. A -> C e. ( A +H B ) ) )
4	3	adantrd	|- ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> C e. ( A +H B ) ) )
5		shsel2	|- ( ( A e. SH /\ B e. SH ) -> ( D e. B -> D e. ( A +H B ) ) )
6	5	adantld	|- ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> D e. ( A +H B ) ) )
7	2 4 6	3jcad	|- ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( ( A +H B ) e. SH /\ C e. ( A +H B ) /\ D e. ( A +H B ) ) ) )
8		shsubcl	|- ( ( ( A +H B ) e. SH /\ C e. ( A +H B ) /\ D e. ( A +H B ) ) -> ( C -h D ) e. ( A +H B ) )
9	7 8	syl6	|- ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( C -h D ) e. ( A +H B ) ) )