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 = ( 1st ` R )
ringgcl.2
|- X = ran G
Assertion rngoaass
|- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )

Proof

Step Hyp Ref Expression
1 ringgcl.1
 |-  G = ( 1st ` R )
2 ringgcl.2
 |-  X = ran G
3 1 rngogrpo
 |-  ( R e. RingOps -> G e. GrpOp )
4 2 grpoass
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )
5 3 4 sylan
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )