Theorem ring1

Description: The (smallest) structure representing azero ring. (Contributed by AV, 28-Apr-2019)

	Ref	Expression
Hypothesis	ring1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}$$
Assertion	ring1	$$⊢Z\in V\to M\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		ring1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}$$
2		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}$$
3	2	grp1	$$⊢Z\in V\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}\in \mathrm{Grp}$$
4		snex	$$⊢\left\{Z\right\}\in \mathrm{V}$$
5	1	rngbase	$$⊢\left\{Z\right\}\in \mathrm{V}\to \left\{Z\right\}={\mathrm{Base}}_M$$
6	4 5	ax-mp	$$⊢\left\{Z\right\}={\mathrm{Base}}_M$$
7	6	eqcomi	$$⊢{\mathrm{Base}}_M=\left\{Z\right\}$$
8		snex	$$⊢\left\{⟨⟨Z,Z⟩,Z⟩\right\}\in \mathrm{V}$$
9	1	rngplusg	$$⊢\left\{⟨⟨Z,Z⟩,Z⟩\right\}\in \mathrm{V}\to \left\{⟨⟨Z,Z⟩,Z⟩\right\}={+}_M$$
10	9	eqcomd	$$⊢\left\{⟨⟨Z,Z⟩,Z⟩\right\}\in \mathrm{V}\to {+}_M=\left\{⟨⟨Z,Z⟩,Z⟩\right\}$$
11	8 10	ax-mp	$$⊢{+}_M=\left\{⟨⟨Z,Z⟩,Z⟩\right\}$$
12	7 11 2	grppropstr	$$⊢M\in \mathrm{Grp}\leftrightarrow \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}\in \mathrm{Grp}$$
13	3 12	sylibr	$$⊢Z\in V\to M\in \mathrm{Grp}$$
14	2	mnd1	$$⊢Z\in V\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}\in \mathrm{Mnd}$$
15		eqid	$$⊢{\mathrm{mulGrp}}_M={\mathrm{mulGrp}}_M$$
16	15 6	mgpbas	$$⊢\left\{Z\right\}={\mathrm{Base}}_{{\mathrm{mulGrp}}_M}$$
17	2	grpbase	$$⊢\left\{Z\right\}\in \mathrm{V}\to \left\{Z\right\}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}}$$
18	4 17	ax-mp	$$⊢\left\{Z\right\}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}}$$
19	16 18	eqtr3i	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_M}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}}$$
20	1	rngmulr	$$⊢\left\{⟨⟨Z,Z⟩,Z⟩\right\}\in \mathrm{V}\to \left\{⟨⟨Z,Z⟩,Z⟩\right\}={\cdot }_M$$
21	8 20	ax-mp	$$⊢\left\{⟨⟨Z,Z⟩,Z⟩\right\}={\cdot }_M$$
22	2	grpplusg	$$⊢\left\{⟨⟨Z,Z⟩,Z⟩\right\}\in \mathrm{V}\to \left\{⟨⟨Z,Z⟩,Z⟩\right\}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}}$$
23	8 22	ax-mp	$$⊢\left\{⟨⟨Z,Z⟩,Z⟩\right\}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}}$$
24		eqid	$$⊢{\cdot }_M={\cdot }_M$$
25	15 24	mgpplusg	$$⊢{\cdot }_M={+}_{{\mathrm{mulGrp}}_M}$$
26	21 23 25	3eqtr3ri	$$⊢{+}_{{\mathrm{mulGrp}}_M}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}}$$
27	19 26	mndprop	$$⊢{\mathrm{mulGrp}}_M\in \mathrm{Mnd}\leftrightarrow \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{Z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right\}\in \mathrm{Mnd}$$
28	14 27	sylibr	$$⊢Z\in V\to {\mathrm{mulGrp}}_M\in \mathrm{Mnd}$$
29		df-ov	$$⊢Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z=\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(⟨Z,Z⟩\right)$$
30		opex	$$⊢⟨Z,Z⟩\in \mathrm{V}$$
31		fvsng	$$⊢\left(⟨Z,Z⟩\in \mathrm{V}\wedge Z\in V\right)\to \left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(⟨Z,Z⟩\right)=Z$$
32	30 31	mpan	$$⊢Z\in V\to \left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(⟨Z,Z⟩\right)=Z$$
33	29 32	syl5eq	$$⊢Z\in V\to Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z=Z$$
34	33	oveq2d	$$⊢Z\in V\to Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z$$
35	33 33	oveq12d	$$⊢Z\in V\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z$$
36	34 35	eqtr4d	$$⊢Z\in V\to Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)$$
37	33	oveq1d	$$⊢Z\in V\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z$$
38	37 35	eqtr4d	$$⊢Z\in V\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)$$
39		oveq1	$$⊢a=Z\to a\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)$$
40		oveq1	$$⊢a=Z\to a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b$$
41		oveq1	$$⊢a=Z\to a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c$$
42	40 41	oveq12d	$$⊢a=Z\to \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)$$
43	39 42	eqeq12d	$$⊢a=Z\to \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\leftrightarrow Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)$$
44	40	oveq1d	$$⊢a=Z\to \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c$$
45	41	oveq1d	$$⊢a=Z\to \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)$$
46	44 45	eqeq12d	$$⊢a=Z\to \left(\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\leftrightarrow \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)$$
47	43 46	anbi12d	$$⊢a=Z\to \left(\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\right)$$
48	47	2ralbidv	$$⊢a=Z\to \left(\forall b\in \left\{Z\right\}\forall c\in \left\{Z\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \forall b\in \left\{Z\right\}\forall c\in \left\{Z\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\right)$$
49	48	ralsng	$$⊢Z\in V\to \left(\forall a\in \left\{Z\right\}\forall b\in \left\{Z\right\}\forall c\in \left\{Z\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \forall b\in \left\{Z\right\}\forall c\in \left\{Z\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\right)$$
50		oveq1	$$⊢b=Z\to b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c$$
51	50	oveq2d	$$⊢b=Z\to Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)$$
52		oveq2	$$⊢b=Z\to Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z$$
53	52	oveq1d	$$⊢b=Z\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)$$
54	51 53	eqeq12d	$$⊢b=Z\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\leftrightarrow Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)$$
55	52	oveq1d	$$⊢b=Z\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c$$
56	50	oveq2d	$$⊢b=Z\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)$$
57	55 56	eqeq12d	$$⊢b=Z\to \left(\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\leftrightarrow \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)$$
58	54 57	anbi12d	$$⊢b=Z\to \left(\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\right)$$
59	58	ralbidv	$$⊢b=Z\to \left(\forall c\in \left\{Z\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \forall c\in \left\{Z\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\right)$$
60	59	ralsng	$$⊢Z\in V\to \left(\forall b\in \left\{Z\right\}\forall c\in \left\{Z\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \forall c\in \left\{Z\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\right)$$
61		oveq2	$$⊢c=Z\to Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z$$
62	61	oveq2d	$$⊢c=Z\to Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)$$
63	61	oveq2d	$$⊢c=Z\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)$$
64	62 63	eqeq12d	$$⊢c=Z\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\leftrightarrow Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\right)$$
65		oveq2	$$⊢c=Z\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z$$
66	61 61	oveq12d	$$⊢c=Z\to \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)$$
67	65 66	eqeq12d	$$⊢c=Z\to \left(\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\leftrightarrow \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\right)$$
68	64 67	anbi12d	$$⊢c=Z\to \left(\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\right)\right)$$
69	68	ralsng	$$⊢Z\in V\to \left(\forall c\in \left\{Z\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\right)\right)$$
70	49 60 69	3bitrd	$$⊢Z\in V\to \left(\forall a\in \left\{Z\right\}\forall b\in \left\{Z\right\}\forall c\in \left\{Z\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\leftrightarrow \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\wedge \left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z=\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(Z\left\{⟨⟨Z,Z⟩,Z⟩\right\}Z\right)\right)\right)$$
71	36 38 70	mpbir2and	$$⊢Z\in V\to \forall a\in \left\{Z\right\}\forall b\in \left\{Z\right\}\forall c\in \left\{Z\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)$$
72	8 9	ax-mp	$$⊢\left\{⟨⟨Z,Z⟩,Z⟩\right\}={+}_M$$
73	6 15 72 21	isring	$$⊢M\in \mathrm{Ring}\leftrightarrow \left(M\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_M\in \mathrm{Mnd}\wedge \forall a\in \left\{Z\right\}\forall b\in \left\{Z\right\}\forall c\in \left\{Z\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\wedge \left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}b\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}c=\left(a\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\left\{⟨⟨Z,Z⟩,Z⟩\right\}\left(b\left\{⟨⟨Z,Z⟩,Z⟩\right\}c\right)\right)\right)$$
74	13 28 71 73	syl3anbrc	$$⊢Z\in V\to M\in \mathrm{Ring}$$