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