Metamath Proof Explorer


Theorem rngoaass

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

Ref Expression
Hypotheses ringgcl.1 G=1stR
ringgcl.2 X=ranG
Assertion rngoaass RRingOpsAXBXCXAGBGC=AGBGC

Proof

Step Hyp Ref Expression
1 ringgcl.1 G=1stR
2 ringgcl.2 X=ranG
3 1 rngogrpo RRingOpsGGrpOp
4 2 grpoass GGrpOpAXBXCXAGBGC=AGBGC
5 3 4 sylan RRingOpsAXBXCXAGBGC=AGBGC