Definition df-edom

Description: Define Euclidean domains. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Assertion	df-edom	$$⊢\mathrm{EDomn}=\left\{d\in \mathrm{IDomn}|\underset{\dot{}}{[}\mathrm{EuclF}\left(d\right)/e\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_d/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left(v\setminus \left\{0_d\right\}\right)/w\underset{\dot{}}{]}\left(\left({e\upharpoonright }_w\right):w⟶{\mathbb{N}}_0\wedge \forall a\in v\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cedom	$$class\mathrm{EDomn}$$
1		vd	$$setvard$$
2		cidom	$$class\mathrm{IDomn}$$
3		ceuf	$$class\mathrm{EuclF}$$
4	1	cv	$$setvard$$
5	4 3	cfv	$$class\mathrm{EuclF}\left(d\right)$$
6		ve	$$setvare$$
7		cbs	$$class\mathrm{Base}$$
8	4 7	cfv	$$class{\mathrm{Base}}_d$$
9		vv	$$setvarv$$
10	9	cv	$$setvarv$$
11		c0g	$$class{0}_{𝑔}$$
12	4 11	cfv	$$class{0}_d$$
13	12	csn	$$class\left\{0_d\right\}$$
14	10 13	cdif	$$class\left(v\setminus \left\{0_d\right\}\right)$$
15		vw	$$setvarw$$
16	6	cv	$$setvare$$
17	15	cv	$$setvarw$$
18	16 17	cres	$$class\left({e\upharpoonright }_w\right)$$
19		cn0	$$class{\mathbb{N}}_0$$
20	17 19 18	wf	$$wff\left({e\upharpoonright }_w\right):w⟶{\mathbb{N}}_0$$
21		va	$$setvara$$
22		vb	$$setvarb$$
23		vq	$$setvarq$$
24		vr	$$setvarr$$
25	21	cv	$$setvara$$
26	22	cv	$$setvarb$$
27		cmulr	$$class{\cdot }_{𝑟}$$
28	4 27	cfv	$$class{\cdot }_d$$
29	23	cv	$$setvarq$$
30	26 29 28	co	$$class\left(b{\cdot }_{d}q\right)$$
31		cplusg	$$class{+}_{𝑔}$$
32	4 31	cfv	$$class{+}_d$$
33	24	cv	$$setvarr$$
34	30 33 32	co	$$class\left(\left(b{\cdot }_{d}q\right){+}_{d}r\right)$$
35	25 34	wceq	$$wffa=\left(b{\cdot }_{d}q\right){+}_{d}r$$
36	33 12	wceq	$$wffr=0_d$$
37	33 16	cfv	$$classe\left(r\right)$$
38		clt	$$class<$$
39	26 16	cfv	$$classe\left(b\right)$$
40	37 39 38	wbr	$$wffe\left(r\right)<e\left(b\right)$$
41	36 40	wo	$$wff\left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)$$
42	35 41	wa	$$wff\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
43	42 24 10	wrex	$$wff\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
44	43 23 10	wrex	$$wff\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
45	44 22 17	wral	$$wff\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
46	45 21 10	wral	$$wff\forall a\in v\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
47	20 46	wa	$$wff\left(\left({e\upharpoonright }_w\right):w⟶{\mathbb{N}}_0\wedge \forall a\in v\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)$$
48	47 15 14	wsbc	$$wff\underset{\dot{}}{[}\left(v\setminus \left\{0_d\right\}\right)/w\underset{\dot{}}{]}\left(\left({e\upharpoonright }_w\right):w⟶{\mathbb{N}}_0\wedge \forall a\in v\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)$$
49	48 9 8	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_d/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left(v\setminus \left\{0_d\right\}\right)/w\underset{\dot{}}{]}\left(\left({e\upharpoonright }_w\right):w⟶{\mathbb{N}}_0\wedge \forall a\in v\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)$$
50	49 6 5	wsbc	$$wff\underset{\dot{}}{[}\mathrm{EuclF}\left(d\right)/e\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_d/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left(v\setminus \left\{0_d\right\}\right)/w\underset{\dot{}}{]}\left(\left({e\upharpoonright }_w\right):w⟶{\mathbb{N}}_0\wedge \forall a\in v\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)$$
51	50 1 2	crab	$$class\left\{d\in \mathrm{IDomn}|\underset{\dot{}}{[}\mathrm{EuclF}\left(d\right)/e\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_d/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left(v\setminus \left\{0_d\right\}\right)/w\underset{\dot{}}{]}\left(\left({e\upharpoonright }_w\right):w⟶{\mathbb{N}}_0\wedge \forall a\in v\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)\right\}$$
52	0 51	wceq	$$wff\mathrm{EDomn}=\left\{d\in \mathrm{IDomn}|\underset{\dot{}}{[}\mathrm{EuclF}\left(d\right)/e\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_d/v\underset{\dot{}}{]}\underset{\dot{}}{[}\left(v\setminus \left\{0_d\right\}\right)/w\underset{\dot{}}{]}\left(\left({e\upharpoonright }_w\right):w⟶{\mathbb{N}}_0\wedge \forall a\in v\forall b\in w\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)\right\}$$