Metamath Proof Explorer


Theorem nvaddsub

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

Proof

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