Definition df-edom 32388

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

Assertion

Ref	Expression
df-edom	⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))}

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

Detailed syntax breakdown of Definition df-edom

Step	Hyp	Ref	Expression
1		cedom 32387	. 2 class EDomn
2		ve	. . . . . . . 8 setvar 𝑒
3	2	cv 1540	. . . . . . 7 class 𝑒
4	3	wfun 6537	. . . . . 6 wff Fun 𝑒
5		vv	. . . . . . . . . 10 setvar 𝑣
6	5	cv 1540	. . . . . . . . 9 class 𝑣
7		vd	. . . . . . . . . . . 12 setvar 𝑑
8	7	cv 1540	. . . . . . . . . . 11 class 𝑑
9		c0g 17384	. . . . . . . . . . 11 class 0g
10	8, 9	cfv 6543	. . . . . . . . . 10 class (0g‘𝑑)
11	10	csn 4628	. . . . . . . . 9 class {(0g‘𝑑)}
12	6, 11	cdif 3945	. . . . . . . 8 class (𝑣 ∖ {(0g‘𝑑)})
13	3, 12	cima 5679	. . . . . . 7 class (𝑒 “ (𝑣 ∖ {(0g‘𝑑)}))
14		cc0 11109	. . . . . . . 8 class 0
15		cpnf 11244	. . . . . . . 8 class +∞
16		cico 13325	. . . . . . . 8 class [,)
17	14, 15, 16	co 7408	. . . . . . 7 class (0[,)+∞)
18	13, 17	wss 3948	. . . . . 6 wff (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞)
19		va	. . . . . . . . . . . . 13 setvar 𝑎
20	19	cv 1540	. . . . . . . . . . . 12 class 𝑎
21		vb	. . . . . . . . . . . . . . 15 setvar 𝑏
22	21	cv 1540	. . . . . . . . . . . . . 14 class 𝑏
23		vq	. . . . . . . . . . . . . . 15 setvar 𝑞
24	23	cv 1540	. . . . . . . . . . . . . 14 class 𝑞
25		cmulr 17197	. . . . . . . . . . . . . . 15 class .r
26	8, 25	cfv 6543	. . . . . . . . . . . . . 14 class (.r‘𝑑)
27	22, 24, 26	co 7408	. . . . . . . . . . . . 13 class (𝑏(.r‘𝑑)𝑞)
28		vr	. . . . . . . . . . . . . 14 setvar 𝑟
29	28	cv 1540	. . . . . . . . . . . . 13 class 𝑟
30		cplusg 17196	. . . . . . . . . . . . . 14 class +g
31	8, 30	cfv 6543	. . . . . . . . . . . . 13 class (+g‘𝑑)
32	27, 29, 31	co 7408	. . . . . . . . . . . 12 class ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟)
33	20, 32	wceq 1541	. . . . . . . . . . 11 wff 𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟)
34	29, 10	wceq 1541	. . . . . . . . . . . 12 wff 𝑟 = (0g‘𝑑)
35	29, 3	cfv 6543	. . . . . . . . . . . . 13 class (𝑒‘𝑟)
36	22, 3	cfv 6543	. . . . . . . . . . . . 13 class (𝑒‘𝑏)
37		clt 11247	. . . . . . . . . . . . 13 class <
38	35, 36, 37	wbr 5148	. . . . . . . . . . . 12 wff (𝑒‘𝑟) < (𝑒‘𝑏)
39	34, 38	wo 845	. . . . . . . . . . 11 wff (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))
40	33, 39	wa 396	. . . . . . . . . 10 wff (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
41	40, 28, 6	wrex 3070	. . . . . . . . 9 wff ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
42	41, 23, 6	wrex 3070	. . . . . . . 8 wff ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
43	42, 21, 12	wral 3061	. . . . . . 7 wff ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
44	43, 19, 6	wral 3061	. . . . . 6 wff ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏)))
45	4, 18, 44	w3a 1087	. . . . 5 wff (Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))
46		cbs 17143	. . . . . 6 class Base
47	8, 46	cfv 6543	. . . . 5 class (Base‘𝑑)
48	45, 5, 47	wsbc 3777	. . . 4 wff [(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))
49		ceuf 32383	. . . . 5 class EuclF
50	8, 49	cfv 6543	. . . 4 class (EuclF‘𝑑)
51	48, 2, 50	wsbc 3777	. . 3 wff [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))
52		cidom 20896	. . 3 class IDomn
53	51, 7, 52	crab 3432	. 2 class {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))}
54	1, 53	wceq 1541	1 wff EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))}

This definition is referenced by: (None)