# Metamath Proof Explorer

## Theorem rngoablo2

Description: In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009) (New usage is discouraged.)

Ref Expression
Assertion rngoablo2 ${⊢}⟨{G},{H}⟩\in \mathrm{RingOps}\to {G}\in \mathrm{AbelOp}$

### Proof

Step Hyp Ref Expression
1 df-br ${⊢}{G}\mathrm{RingOps}{H}↔⟨{G},{H}⟩\in \mathrm{RingOps}$
2 relrngo ${⊢}\mathrm{Rel}\mathrm{RingOps}$
3 2 brrelex12i ${⊢}{G}\mathrm{RingOps}{H}\to \left({G}\in \mathrm{V}\wedge {H}\in \mathrm{V}\right)$
4 op1stg ${⊢}\left({G}\in \mathrm{V}\wedge {H}\in \mathrm{V}\right)\to {1}^{st}\left(⟨{G},{H}⟩\right)={G}$
5 3 4 syl ${⊢}{G}\mathrm{RingOps}{H}\to {1}^{st}\left(⟨{G},{H}⟩\right)={G}$
6 1 5 sylbir ${⊢}⟨{G},{H}⟩\in \mathrm{RingOps}\to {1}^{st}\left(⟨{G},{H}⟩\right)={G}$
7 eqid ${⊢}{1}^{st}\left(⟨{G},{H}⟩\right)={1}^{st}\left(⟨{G},{H}⟩\right)$
8 7 rngoablo ${⊢}⟨{G},{H}⟩\in \mathrm{RingOps}\to {1}^{st}\left(⟨{G},{H}⟩\right)\in \mathrm{AbelOp}$
9 6 8 eqeltrrd ${⊢}⟨{G},{H}⟩\in \mathrm{RingOps}\to {G}\in \mathrm{AbelOp}$