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