Theorem rngoablo

Description: Obsolete theorem, use ringabl instead. 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.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	ringabl.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
Assertion	rngoablo	⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ AbelOp )

Proof

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 )