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	⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → 𝐺 ∈ AbelOp )

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐺 RingOps 𝐻 ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps )
2		relrngo	⊢ Rel RingOps
3	2	brrelex12i	⊢ ( 𝐺 RingOps 𝐻 → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
4		op1stg	⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( 1^st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐺 )
5	3 4	syl	⊢ ( 𝐺 RingOps 𝐻 → ( 1^st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐺 )
6	1 5	sylbir	⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → ( 1^st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐺 )
7		eqid	⊢ ( 1^st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = ( 1^st ‘ ⟨ 𝐺 , 𝐻 ⟩ )
8	7	rngoablo	⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → ( 1^st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) ∈ AbelOp )
9	6 8	eqeltrrd	⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → 𝐺 ∈ AbelOp )

Metamath Proof Explorer