Theorem ringabl

Description: A ring is an Abelian group. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by NM, 26-Aug-2011)

	Ref	Expression
Assertion	ringabl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
2		eqidd	⊢ ( 𝑅 ∈ Ring → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
3		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6	4 5	ringcom	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) )
7	1 2 3 6	isabld	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )