Description: A ring is an Abelian group. (Contributed by NM, 26-Aug-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | ringabl | ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel ) |
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 ) |