This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngabl

Description: A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020)

Ref Expression
Assertion rngabl ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
3 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
4 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5 1 2 3 4 isrng ⊢ ( 𝑅 ∈ Rng ↔ ( 𝑅 ∈ Abel ∧ ( mulGrp ‘ 𝑅 ) ∈ Smgrp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) ) )
6 5 simp1bi ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )