Metamath Proof Explorer


Theorem shsvs

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

Ref Expression
Assertion shsvs ASBSCADBC-DA+B

Proof

Step Hyp Ref Expression
1 shscl ASBSA+BS
2 1 a1d ASBSCADBA+BS
3 shsel1 ASBSCACA+B
4 3 adantrd ASBSCADBCA+B
5 shsel2 ASBSDBDA+B
6 5 adantld ASBSCADBDA+B
7 2 4 6 3jcad ASBSCADBA+BSCA+BDA+B
8 shsubcl A+BSCA+BDA+BC-DA+B
9 7 8 syl6 ASBSCADBC-DA+B