Definition df-edom 33933

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

Assertion

Ref	Expression
df-edom	⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣][(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))}

Distinct variable group:   𝑎,𝑏,𝑑,𝑒,𝑞,𝑟,𝑣,𝑤

Detailed syntax breakdown of Definition df-edom

Step	Hyp	Ref	Expression
1		cedom 33932	. 2 class EDomn
2		vw	. . . . . . . . 9 setvar 𝑤
3	2	cv 1569	. . . . . . . 8 class 𝑤
4		cn0 12636	. . . . . . . 8 class ℕ0
5		ve	. . . . . . . . . 10 setvar 𝑒
6	5	cv 1569	. . . . . . . . 9 class 𝑒
7	6, 3	cres 5658	. . . . . . . 8 class (𝑒 ↾ 𝑤)
8	3, 4, 7	wf 6557	. . . . . . 7 wff (𝑒 ↾ 𝑤):𝑤⟶ℕ0
9		va	. . . . . . . . . . . . . 14 setvar 𝑎
10	9	cv 1569	. . . . . . . . . . . . 13 class 𝑎
11		vb	. . . . . . . . . . . . . . . 16 setvar 𝑏
12	11	cv 1569	. . . . . . . . . . . . . . 15 class 𝑏
13		vq	. . . . . . . . . . . . . . . 16 setvar 𝑞
14	13	cv 1569	. . . . . . . . . . . . . . 15 class 𝑞
15		vd	. . . . . . . . . . . . . . . . 17 setvar 𝑑
16	15	cv 1569	. . . . . . . . . . . . . . . 16 class 𝑑
17		cmulr 17461	. . . . . . . . . . . . . . . 16 class .r
18	16, 17	cfv 6561	. . . . . . . . . . . . . . 15 class (.r‘𝑑)
19	12, 14, 18	co 7446	. . . . . . . . . . . . . 14 class (𝑏(.r‘𝑑)𝑞)
20		vr	. . . . . . . . . . . . . . 15 setvar 𝑟
21	20	cv 1569	. . . . . . . . . . . . . 14 class 𝑟
22		cplusg 17460	. . . . . . . . . . . . . . 15 class +g
23	16, 22	cfv 6561	. . . . . . . . . . . . . 14 class (+g‘𝑑)
24	19, 21, 23	co 7446	. . . . . . . . . . . . 13 class ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟)
25	10, 24	wceq 1570	. . . . . . . . . . . 12 wff 𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟)
26		c0g 17642	. . . . . . . . . . . . . . 15 class 0g
27	16, 26	cfv 6561	. . . . . . . . . . . . . 14 class (0g‘𝑑)
28	21, 27	wceq 1570	. . . . . . . . . . . . 13 wff 𝑟 = (0g‘𝑑)
29	21, 6	cfv 6561	. . . . . . . . . . . . . 14 class (𝑒‘𝑟)
30	12, 6	cfv 6561	. . . . . . . . . . . . . 14 class (𝑒‘𝑏)
31		clt 11373	. . . . . . . . . . . . . 14 class <
32	29, 30, 31	wbr 5106	. . . . . . . . . . . . 13 wff (𝑒‘𝑟) < (𝑒‘𝑏)
33	28, 32	wo 861	. . . . . . . . . . . 12 wff (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))
34	25, 33	wa 401	. . . . . . . . . . 11 wff (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
35		vv	. . . . . . . . . . . 12 setvar 𝑣
36	35	cv 1569	. . . . . . . . . . 11 class 𝑣
37	34, 20, 36	wrex 3090	. . . . . . . . . 10 wff ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
38	37, 13, 36	wrex 3090	. . . . . . . . 9 wff ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
39	38, 11, 3	wral 3080	. . . . . . . 8 wff ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
40	39, 9, 36	wral 3080	. . . . . . 7 wff ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
41	8, 40	wa 401	. . . . . 6 wff ((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))
42	27	csn 4588	. . . . . . 7 class {(0g‘𝑑)}
43	36, 42	cdif 4048	. . . . . 6 class (𝑣 ∖ {(0g‘𝑑)})
44	41, 2, 43	wsbc 3742	. . . . 5 wff [(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))
45		cbs 17419	. . . . . 6 class Base
46	16, 45	cfv 6561	. . . . 5 class (Base‘𝑑)
47	44, 35, 46	wsbc 3742	. . . 4 wff [(Base‘𝑑) / 𝑣][(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))
48		ceuf 33928	. . . . 5 class EuclF
49	16, 48	cfv 6561	. . . 4 class (EuclF‘𝑑)
50	47, 5, 49	wsbc 3742	. . 3 wff [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣][(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))
51		cidom 20978	. . 3 class IDomn
52	50, 15, 51	crab 3416	. 2 class {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣][(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))}
53	1, 52	wceq 1570	1 wff EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣][(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))}

This definition is used by:  isedom  33934