Metamath Proof Explorer


Theorem nvcom

Description: The vector addition (group) operation is commutative. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

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

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 ablocom
 |-  ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )
6 3 5 syl3an1
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )