Description: Commutative/associative law for vector addition and subtraction. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nvpncan2.1 | |- X = ( BaseSet ` U ) |
|
| nvpncan2.2 | |- G = ( +v ` U ) |
||
| nvpncan2.3 | |- M = ( -v ` U ) |
||
| Assertion | nvaddsub | |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) M C ) = ( ( A M C ) G B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nvpncan2.1 | |- X = ( BaseSet ` U ) |
|
| 2 | nvpncan2.2 | |- G = ( +v ` U ) |
|
| 3 | nvpncan2.3 | |- M = ( -v ` U ) |
|
| 4 | 2 | nvablo | |- ( U e. NrmCVec -> G e. AbelOp ) |
| 5 | 1 2 | bafval | |- X = ran G |
| 6 | 2 3 | vsfval | |- M = ( /g ` G ) |
| 7 | 5 6 | ablomuldiv | |- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) M C ) = ( ( A M C ) G B ) ) |
| 8 | 4 7 | sylan | |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) M C ) = ( ( A M C ) G B ) ) |