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	$$⊢B={\mathrm{Base}}_R$$
	isringrng.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	dfring2.g	$$⊢G={\mathrm{mulGrp}}_R$$
	dfring2.p	$$⊢\underset{\dot{}}{+}={+}_R$$
Assertion	dfring2	$$⊢R\in \mathrm{Ring}\leftrightarrow \left(R\in \mathrm{Abel}\wedge G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isringrng.b	$$⊢B={\mathrm{Base}}_R$$
2		isringrng.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		dfring2.g	$$⊢G={\mathrm{mulGrp}}_R$$
4		dfring2.p	$$⊢\underset{\dot{}}{+}={+}_R$$
5		ringabl	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Abel}$$
6	3	ringmgp	$$⊢R\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
7	1 3 4 2	isring	$$⊢R\in \mathrm{Ring}\leftrightarrow \left(R\in \mathrm{Grp}\wedge G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
8	7	simp3bi	$$⊢R\in \mathrm{Ring}\to \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)$$
9	5 6 8	3jca	$$⊢R\in \mathrm{Ring}\to \left(R\in \mathrm{Abel}\wedge G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
10		ablgrp	$$⊢R\in \mathrm{Abel}\to R\in \mathrm{Grp}$$
11	10	3anim1i	$$⊢\left(R\in \mathrm{Abel}\wedge G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)\to \left(R\in \mathrm{Grp}\wedge G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
12	11 7	sylibr	$$⊢\left(R\in \mathrm{Abel}\wedge G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)\to R\in \mathrm{Ring}$$
13	9 12	impbii	$$⊢R\in \mathrm{Ring}\leftrightarrow \left(R\in \mathrm{Abel}\wedge G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$