dfring3

Description: The predicate "is a (unital) ring" based on a ring being abelian and with the definition of a monoid expanded. (Contributed by Jeff Hankins, 21-Nov-2006) (Revised by AV, 24-Aug-2026)

	Ref	Expression
Hypotheses	isringrng.b	$⊢ B = {Base}_{R}$
	isringrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	dfring2.g	$⊢ G = {mulGrp}_{R}$
	dfring2.p	$⊢ \underset{˙}{+} = +_{R}$
Assertion	dfring3	$⊢ R \in Ring \leftrightarrow ((R \in Abel \land G \in Mgm) \land \forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$

Proof

Step	Hyp	Ref	Expression
1		isringrng.b	$⊢ B = {Base}_{R}$
2		isringrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		dfring2.g	$⊢ G = {mulGrp}_{R}$
4		dfring2.p	$⊢ \underset{˙}{+} = +_{R}$
5	1 2 3 4	dfring2	$⊢ R \in Ring \leftrightarrow (R \in Abel \land G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
6	3 1	mgpbas	$⊢ B = {Base}_{G}$
7	3 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{G}$
8	6 7	ismnddef	$⊢ G \in Mnd \leftrightarrow (G \in Smgrp \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
9	6 7	issgrp	$⊢ G \in Smgrp \leftrightarrow (G \in Mgm \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z))$
10	8 9	bianbi	$⊢ G \in Mnd \leftrightarrow ((G \in Mgm \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
11	10	anbi1i	$⊢ (G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (((G \in Mgm \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
12		anass	$⊢ (((G \in Mgm \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow ((G \in Mgm \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)) \land (\exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))))$
13		anass	$⊢ ((G \in Mgm \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)) \land (\exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))) \leftrightarrow (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (\exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))))$
14	12 13	bitri	$⊢ (((G \in Mgm \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (\exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))))$
15		ancom	$⊢ (\exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
16	15	anbi2i	$⊢ (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (\exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))) \leftrightarrow (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)))$
17		anass	$⊢ ((\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \leftrightarrow (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)))$
18		r19.26-2	$⊢ \forall x \in B \forall y \in B (\forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
19		r19.26	$⊢ \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (\forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
20		3anass	$⊢ ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
21	20	bicomi	$⊢ ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
22	21	ralbii	$⊢ \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
23	19 22	bitr3i	$⊢ (\forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
24	23	2ralbii	$⊢ \forall x \in B \forall y \in B (\forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
25	18 24	bitr3i	$⊢ (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
26	25	anbi1i	$⊢ ((\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \leftrightarrow (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
27	17 26	bitr3i	$⊢ (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))) \leftrightarrow (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
28	16 27	bitri	$⊢ (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (\exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))) \leftrightarrow (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
29	28	anbi2i	$⊢ (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land (\exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))))) \leftrightarrow (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)))$
30	14 29	bitri	$⊢ (((G \in Mgm \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)))$
31	11 30	bitri	$⊢ (G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)))$
32	31	anbi2i	$⊢ (R \in Abel \land (G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))) \leftrightarrow (R \in Abel \land (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))))$
33		3anass	$⊢ (R \in Abel \land G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (R \in Abel \land (G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))))$
34		3anass	$⊢ ((R \in Abel \land G \in Mgm) \land \forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \leftrightarrow ((R \in Abel \land G \in Mgm) \land (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)))$
35		anass	$⊢ ((R \in Abel \land G \in Mgm) \land (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))) \leftrightarrow (R \in Abel \land (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))))$
36	34 35	bitri	$⊢ ((R \in Abel \land G \in Mgm) \land \forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y)) \leftrightarrow (R \in Abel \land (G \in Mgm \land (\forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))))$
37	32 33 36	3bitr4i	$⊢ (R \in Abel \land G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow ((R \in Abel \land G \in Mgm) \land \forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$
38	5 37	bitri	$⊢ R \in Ring \leftrightarrow ((R \in Abel \land G \in Mgm) \land \forall x \in B \forall y \in B \forall z \in B ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \land x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land \exists x \in B \forall y \in B (x \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} x = y))$

Metamath Proof Explorer

Theorem dfring3

Proof