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 RingOps \to G \in AbelOp$

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

Metamath Proof Explorer