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