Theorem dfring2

Description: The predicate "is a unital ring" based on a ring being abelian. Definition of "ring with unit" in Lang p. 83. (Contributed by Jeff Hankins, 21-Nov-2006) (Revised by AV, 8-Aug-2026)

	Ref	Expression
Hypotheses	isringrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isringrng.t	⊢ · = ( .r ‘ 𝑅 )
	dfring2.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	dfring2.p	⊢ + = ( +g ‘ 𝑅 )
Assertion	dfring2	⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Abel ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isringrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isringrng.t	⊢ · = ( .r ‘ 𝑅 )
3		dfring2.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
4		dfring2.p	⊢ + = ( +g ‘ 𝑅 )
5		ringabl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
6	3	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Mnd )
7	1 3 4 2	isring	⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
8	7	simp3bi	⊢ ( 𝑅 ∈ Ring → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
9	5 6 8	3jca	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ Abel ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
10		ablgrp	⊢ ( 𝑅 ∈ Abel → 𝑅 ∈ Grp )
11	10	3anim1i	⊢ ( ( 𝑅 ∈ Abel ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) → ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
12	11 7	sylibr	⊢ ( ( 𝑅 ∈ Abel ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) → 𝑅 ∈ Ring )
13	9 12	impbii	⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Abel ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )