# Metamath Proof Explorer

## Definition df-rngo

Description: Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006) (New usage is discouraged.)

Ref Expression
Assertion df-rngo ${⊢}\mathrm{RingOps}=\left\{⟨{g},{h}⟩|\left(\left({g}\in \mathrm{AbelOp}\wedge {h}:\mathrm{ran}{g}×\mathrm{ran}{g}⟶\mathrm{ran}{g}\right)\wedge \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)\wedge \exists {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 crngo ${class}\mathrm{RingOps}$
1 vg ${setvar}{g}$
2 vh ${setvar}{h}$
3 1 cv ${setvar}{g}$
4 cablo ${class}\mathrm{AbelOp}$
5 3 4 wcel ${wff}{g}\in \mathrm{AbelOp}$
6 2 cv ${setvar}{h}$
7 3 crn ${class}\mathrm{ran}{g}$
8 7 7 cxp ${class}\left(\mathrm{ran}{g}×\mathrm{ran}{g}\right)$
9 8 7 6 wf ${wff}{h}:\mathrm{ran}{g}×\mathrm{ran}{g}⟶\mathrm{ran}{g}$
10 5 9 wa ${wff}\left({g}\in \mathrm{AbelOp}\wedge {h}:\mathrm{ran}{g}×\mathrm{ran}{g}⟶\mathrm{ran}{g}\right)$
11 vx ${setvar}{x}$
12 vy ${setvar}{y}$
13 vz ${setvar}{z}$
14 11 cv ${setvar}{x}$
15 12 cv ${setvar}{y}$
16 14 15 6 co ${class}\left({x}{h}{y}\right)$
17 13 cv ${setvar}{z}$
18 16 17 6 co ${class}\left(\left({x}{h}{y}\right){h}{z}\right)$
19 15 17 6 co ${class}\left({y}{h}{z}\right)$
20 14 19 6 co ${class}\left({x}{h}\left({y}{h}{z}\right)\right)$
21 18 20 wceq ${wff}\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)$
22 15 17 3 co ${class}\left({y}{g}{z}\right)$
23 14 22 6 co ${class}\left({x}{h}\left({y}{g}{z}\right)\right)$
24 14 17 6 co ${class}\left({x}{h}{z}\right)$
25 16 24 3 co ${class}\left(\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\right)$
26 23 25 wceq ${wff}{x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)$
27 14 15 3 co ${class}\left({x}{g}{y}\right)$
28 27 17 6 co ${class}\left(\left({x}{g}{y}\right){h}{z}\right)$
29 24 19 3 co ${class}\left(\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)$
30 28 29 wceq ${wff}\left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)$
31 21 26 30 w3a ${wff}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)$
32 31 13 7 wral ${wff}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)$
33 32 12 7 wral ${wff}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)$
34 33 11 7 wral ${wff}\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)$
35 16 15 wceq ${wff}{x}{h}{y}={y}$
36 15 14 6 co ${class}\left({y}{h}{x}\right)$
37 36 15 wceq ${wff}{y}{h}{x}={y}$
38 35 37 wa ${wff}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)$
39 38 12 7 wral ${wff}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)$
40 39 11 7 wrex ${wff}\exists {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)$
41 34 40 wa ${wff}\left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)\wedge \exists {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)\right)$
42 10 41 wa ${wff}\left(\left({g}\in \mathrm{AbelOp}\wedge {h}:\mathrm{ran}{g}×\mathrm{ran}{g}⟶\mathrm{ran}{g}\right)\wedge \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)\wedge \exists {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)\right)\right)$
43 42 1 2 copab ${class}\left\{⟨{g},{h}⟩|\left(\left({g}\in \mathrm{AbelOp}\wedge {h}:\mathrm{ran}{g}×\mathrm{ran}{g}⟶\mathrm{ran}{g}\right)\wedge \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)\wedge \exists {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)\right)\right)\right\}$
44 0 43 wceq ${wff}\mathrm{RingOps}=\left\{⟨{g},{h}⟩|\left(\left({g}\in \mathrm{AbelOp}\wedge {h}:\mathrm{ran}{g}×\mathrm{ran}{g}⟶\mathrm{ran}{g}\right)\wedge \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)\wedge \exists {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)\right)\right)\right\}$