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{}}{]}\left(\mathrm{Fun}e\wedge e\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)\wedge \forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\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	6	cv	$$setvare$$
11	10	wfun	$$wff\mathrm{Fun}e$$
12	9	cv	$$setvarv$$
13		c0g	$$class{0}_{𝑔}$$
14	4 13	cfv	$$class{0}_d$$
15	14	csn	$$class\left\{0_d\right\}$$
16	12 15	cdif	$$class\left(v\setminus \left\{0_d\right\}\right)$$
17	10 16	cima	$$classe\left[v\setminus \left\{0_d\right\}\right]$$
18		cc0	$$class0$$
19		cico	$$class\left[.\right)$$
20		cpnf	$$class\mathrm{+\infty }$$
21	18 20 19	co	$$class\left[0,\mathrm{+\infty }\right)$$
22	17 21	wss	$$wffe\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)$$
23		va	$$setvara$$
24		vb	$$setvarb$$
25		vq	$$setvarq$$
26		vr	$$setvarr$$
27	23	cv	$$setvara$$
28	24	cv	$$setvarb$$
29		cmulr	$$class{\cdot }_{𝑟}$$
30	4 29	cfv	$$class{\cdot }_d$$
31	25	cv	$$setvarq$$
32	28 31 30	co	$$class\left(b{\cdot }_{d}q\right)$$
33		cplusg	$$class{+}_{𝑔}$$
34	4 33	cfv	$$class{+}_d$$
35	26	cv	$$setvarr$$
36	32 35 34	co	$$class\left(\left(b{\cdot }_{d}q\right){+}_{d}r\right)$$
37	27 36	wceq	$$wffa=\left(b{\cdot }_{d}q\right){+}_{d}r$$
38	35 14	wceq	$$wffr=0_d$$
39	35 10	cfv	$$classe\left(r\right)$$
40		clt	$$class<$$
41	28 10	cfv	$$classe\left(b\right)$$
42	39 41 40	wbr	$$wffe\left(r\right)<e\left(b\right)$$
43	38 42	wo	$$wff\left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)$$
44	37 43	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)$$
45	44 26 12	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)$$
46	45 25 12	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)$$
47	46 24 16	wral	$$wff\forall b\in \left(v\setminus \left\{0_d\right\}\right)\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)$$
48	47 23 12	wral	$$wff\forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\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)$$
49	11 22 48	w3a	$$wff\left(\mathrm{Fun}e\wedge e\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)\wedge \forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\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 9 8	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_d/v\underset{\dot{}}{]}\left(\mathrm{Fun}e\wedge e\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)\wedge \forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\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 6 5	wsbc	$$wff\underset{\dot{}}{[}\mathrm{EuclF}\left(d\right)/e\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_d/v\underset{\dot{}}{]}\left(\mathrm{Fun}e\wedge e\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)\wedge \forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\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)$$
52	51 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{}}{]}\left(\mathrm{Fun}e\wedge e\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)\wedge \forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\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\}$$
53	0 52	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{}}{]}\left(\mathrm{Fun}e\wedge e\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)\wedge \forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\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\}$$