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 >. e. RingOps -> G e. AbelOp )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( G RingOps H <-> <. G , H >. e. RingOps )
2 relrngo 
 |-  Rel RingOps
3 2 brrelex12i 
 |-  ( G RingOps H -> ( G e. _V /\ H e. _V ) )
4 op1stg 
 |-  ( ( G e. _V /\ H e. _V ) -> ( 1st ` <. G , H >. ) = G )
5 3 4 syl 
 |-  ( G RingOps H -> ( 1st ` <. G , H >. ) = G )
6 1 5 sylbir 
 |-  ( <. G , H >. e. RingOps -> ( 1st ` <. G , H >. ) = G )
7 eqid 
 |-  ( 1st ` <. G , H >. ) = ( 1st ` <. G , H >. )
8 7 rngoablo 
 |-  ( <. G , H >. e. RingOps -> ( 1st ` <. G , H >. ) e. AbelOp )
9 6 8 eqeltrrd 
 |-  ( <. G , H >. e. RingOps -> G e. AbelOp )