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 | ⊢ 𝐺 = ( 1st ‘ 𝑅 ) | |
| Assertion | rngoablo | ⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ AbelOp ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ringabl.1 | ⊢ 𝐺 = ( 1st ‘ 𝑅 ) | |
| 2 | eqid | ⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 ) | |
| 3 | eqid | ⊢ ran 𝐺 = ran 𝐺 | |
| 4 | 1 2 3 | rngoi | ⊢ ( 𝑅 ∈ RingOps → ( ( 𝐺 ∈ AbelOp ∧ ( 2nd ‘ 𝑅 ) : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) ∧ ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ( 2nd ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( 2nd ‘ 𝑅 ) ( 𝑦 ( 2nd ‘ 𝑅 ) 𝑧 ) ) ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) 𝐺 ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) ( 2nd ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) 𝐺 ( 𝑦 ( 2nd ‘ 𝑅 ) 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( 2nd ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) ) ) |
| 5 | 4 | simplld | ⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ AbelOp ) |