Metamath Proof Explorer


Theorem rngocom

Description: The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ringgcl.1 G=1stR
ringgcl.2 X=ranG
Assertion rngocom RRingOpsAXBXAGB=BGA

Proof

Step Hyp Ref Expression
1 ringgcl.1 G=1stR
2 ringgcl.2 X=ranG
3 1 rngoablo RRingOpsGAbelOp
4 2 ablocom GAbelOpAXBXAGB=BGA
5 3 4 syl3an1 RRingOpsAXBXAGB=BGA