Metamath Proof Explorer


Theorem nvadd32

Description: Commutative/associative law for vector addition. (Contributed by NM, 27-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvgcl.1
|- X = ( BaseSet ` U )
nvgcl.2
|- G = ( +v ` U )
Assertion nvadd32
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )

Proof

Step Hyp Ref Expression
1 nvgcl.1
 |-  X = ( BaseSet ` U )
2 nvgcl.2
 |-  G = ( +v ` U )
3 2 nvablo
 |-  ( U e. NrmCVec -> G e. AbelOp )
4 1 2 bafval
 |-  X = ran G
5 4 ablo32
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )
6 3 5 sylan
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )