Definition df-domn

Description: Adomain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015)

	Ref	Expression
Assertion	df-domn	$$⊢\mathrm{Domn}=\left\{r\in \mathrm{NzRing}|\underset{\dot{}}{[}{\mathrm{Base}}_r/b\underset{\dot{}}{]}\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdomn	$$class\mathrm{Domn}$$
1		vr	$$setvarr$$
2		cnzr	$$class\mathrm{NzRing}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class{\mathrm{Base}}_r$$
6		vb	$$setvarb$$
7		c0g	$$class{0}_{𝑔}$$
8	4 7	cfv	$$class{0}_r$$
9		vz	$$setvarz$$
10		vx	$$setvarx$$
11	6	cv	$$setvarb$$
12		vy	$$setvary$$
13	10	cv	$$setvarx$$
14		cmulr	$$class{\cdot }_{𝑟}$$
15	4 14	cfv	$$class{\cdot }_r$$
16	12	cv	$$setvary$$
17	13 16 15	co	$$class\left(x{\cdot }_{r}y\right)$$
18	9	cv	$$setvarz$$
19	17 18	wceq	$$wffx{\cdot }_{r}y=z$$
20	13 18	wceq	$$wffx=z$$
21	16 18	wceq	$$wffy=z$$
22	20 21	wo	$$wff\left(x=z\vee y=z\right)$$
23	19 22	wi	$$wff\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)$$
24	23 12 11	wral	$$wff\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)$$
25	24 10 11	wral	$$wff\forall x\in b\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)$$
26	25 9 8	wsbc	$$wff\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)$$
27	26 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_r/b\underset{\dot{}}{]}\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)$$
28	27 1 2	crab	$$class\left\{r\in \mathrm{NzRing}|\underset{\dot{}}{[}{\mathrm{Base}}_r/b\underset{\dot{}}{]}\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)\right\}$$
29	0 28	wceq	$$wff\mathrm{Domn}=\left\{r\in \mathrm{NzRing}|\underset{\dot{}}{[}{\mathrm{Base}}_r/b\underset{\dot{}}{]}\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)\right\}$$