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 = ( 1st ` R ) |
|
| Assertion | rngoablo | |- ( R e. RingOps -> G e. AbelOp ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ringabl.1 | |- G = ( 1st ` R ) |
|
| 2 | eqid | |- ( 2nd ` R ) = ( 2nd ` R ) |
|
| 3 | eqid | |- ran G = ran G |
|
| 4 | 1 2 3 | rngoi | |- ( R e. RingOps -> ( ( G e. AbelOp /\ ( 2nd ` R ) : ( ran G X. ran G ) --> ran G ) /\ ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( ( x ( 2nd ` R ) y ) ( 2nd ` R ) z ) = ( x ( 2nd ` R ) ( y ( 2nd ` R ) z ) ) /\ ( x ( 2nd ` R ) ( y G z ) ) = ( ( x ( 2nd ` R ) y ) G ( x ( 2nd ` R ) z ) ) /\ ( ( x G y ) ( 2nd ` R ) z ) = ( ( x ( 2nd ` R ) z ) G ( y ( 2nd ` R ) z ) ) ) /\ E. x e. ran G A. y e. ran G ( ( x ( 2nd ` R ) y ) = y /\ ( y ( 2nd ` R ) x ) = y ) ) ) ) |
| 5 | 4 | simplld | |- ( R e. RingOps -> G e. AbelOp ) |