Theorem isdomn

Description: Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015)

	Ref	Expression
Hypotheses	isdomn.b	$$⊢B={\mathrm{Base}}_R$$
	isdomn.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isdomn.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	isdomn	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isdomn.b	$$⊢B={\mathrm{Base}}_R$$
2		isdomn.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		isdomn.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		fvexd	$$⊢r=R\to {\mathrm{Base}}_r\in \mathrm{V}$$
5		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
6	5 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
7		fvexd	$$⊢\left(r=R\wedge b=B\right)\to 0_r\in \mathrm{V}$$
8		fveq2	$$⊢r=R\to 0_r=0_R$$
9	8	adantr	$$⊢\left(r=R\wedge b=B\right)\to 0_r=0_R$$
10	9 3	eqtr4di	$$⊢\left(r=R\wedge b=B\right)\to 0_r=\underset{\dot{}}{0}$$
11		simplr	$$⊢\left(\left(r=R\wedge b=B\right)\wedge z=\underset{\dot{}}{0}\right)\to b=B$$
12		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
13	12 2	eqtr4di	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
14	13	oveqdr	$$⊢\left(r=R\wedge b=B\right)\to x{\cdot }_{r}y=x\underset{\dot{}}{·}y$$
15		id	$$⊢z=\underset{\dot{}}{0}\to z=\underset{\dot{}}{0}$$
16	14 15	eqeqan12d	$$⊢\left(\left(r=R\wedge b=B\right)\wedge z=\underset{\dot{}}{0}\right)\to \left(x{\cdot }_{r}y=z\leftrightarrow x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\right)$$
17		eqeq2	$$⊢z=\underset{\dot{}}{0}\to \left(x=z\leftrightarrow x=\underset{\dot{}}{0}\right)$$
18		eqeq2	$$⊢z=\underset{\dot{}}{0}\to \left(y=z\leftrightarrow y=\underset{\dot{}}{0}\right)$$
19	17 18	orbi12d	$$⊢z=\underset{\dot{}}{0}\to \left(\left(x=z\vee y=z\right)\leftrightarrow \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)$$
20	19	adantl	$$⊢\left(\left(r=R\wedge b=B\right)\wedge z=\underset{\dot{}}{0}\right)\to \left(\left(x=z\vee y=z\right)\leftrightarrow \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)$$
21	16 20	imbi12d	$$⊢\left(\left(r=R\wedge b=B\right)\wedge z=\underset{\dot{}}{0}\right)\to \left(\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)\leftrightarrow \left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$
22	11 21	raleqbidv	$$⊢\left(\left(r=R\wedge b=B\right)\wedge z=\underset{\dot{}}{0}\right)\to \left(\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)\leftrightarrow \forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$
23	11 22	raleqbidv	$$⊢\left(\left(r=R\wedge b=B\right)\wedge z=\underset{\dot{}}{0}\right)\to \left(\forall x\in b\forall y\in b\left(x{\cdot }_{r}y=z\to \left(x=z\vee y=z\right)\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$
24	7 10 23	sbcied2	$$⊢\left(r=R\wedge b=B\right)\to \left(\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)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$
25	4 6 24	sbcied2	$$⊢r=R\to \left(\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)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$
26		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\}$$
27	25 26	elrab2	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to \left(x=\underset{\dot{}}{0}\vee y=\underset{\dot{}}{0}\right)\right)\right)$$