Metamath Proof Explorer


Theorem rngoablo

Description: A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis ringabl.1 G=1stR
Assertion rngoablo RRingOpsGAbelOp

Proof

Step Hyp Ref Expression
1 ringabl.1 G=1stR
2 eqid 2ndR=2ndR
3 eqid ranG=ranG
4 1 2 3 rngoi RRingOpsGAbelOp2ndR:ranG×ranGranGxranGyranGzranGx2ndRy2ndRz=x2ndRy2ndRzx2ndRyGz=x2ndRyGx2ndRzxGy2ndRz=x2ndRzGy2ndRzxranGyranGx2ndRy=yy2ndRx=y
5 4 simplld RRingOpsGAbelOp