# Metamath Proof Explorer

## 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}↔\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}↔\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)↔{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)↔\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)↔\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\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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)↔\forall {b}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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\}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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)↔\forall {b}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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)↔{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)↔\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)↔\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\}\phantom{\rule{.4em}{0ex}}\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)↔\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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)↔\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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)↔{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)↔\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)↔\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\}\phantom{\rule{.4em}{0ex}}\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)↔\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\}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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)↔\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\}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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}↔\left({M}\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_{{M}}\in \mathrm{Mnd}\wedge \forall {a}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\forall {c}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\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}$