Definition df-edom

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cedom	⊢ EDomn
1		vd	⊢ 𝑑
2		cidom	⊢ IDomn
3		ceuf	⊢ EuclF
4	1	cv	⊢ 𝑑
5	4 3	cfv	⊢ ( EuclF ‘ 𝑑 )
6		ve	⊢ 𝑒
7		cbs	⊢ Base
8	4 7	cfv	⊢ ( Base ‘ 𝑑 )
9		vv	⊢ 𝑣
10	6	cv	⊢ 𝑒
11	10	wfun	⊢ Fun 𝑒
12	9	cv	⊢ 𝑣
13		c0g	⊢ 0g
14	4 13	cfv	⊢ ( 0g ‘ 𝑑 )
15	14	csn	⊢ { ( 0g ‘ 𝑑 ) }
16	12 15	cdif	⊢ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } )
17	10 16	cima	⊢ ( 𝑒 “ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) )
18		cc0	⊢ 0
19		cico	⊢ [,)
20		cpnf	⊢ +∞
21	18 20 19	co	⊢ ( 0 [,) +∞ )
22	17 21	wss	⊢ ( 𝑒 “ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) ⊆ ( 0 [,) +∞ )
23		va	⊢ 𝑎
24		vb	⊢ 𝑏
25		vq	⊢ 𝑞
26		vr	⊢ 𝑟
27	23	cv	⊢ 𝑎
28	24	cv	⊢ 𝑏
29		cmulr	⊢ .r
30	4 29	cfv	⊢ ( .r ‘ 𝑑 )
31	25	cv	⊢ 𝑞
32	28 31 30	co	⊢ ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 )
33		cplusg	⊢ +g
34	4 33	cfv	⊢ ( +g ‘ 𝑑 )
35	26	cv	⊢ 𝑟
36	32 35 34	co	⊢ ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 )
37	27 36	wceq	⊢ 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 )
38	35 14	wceq	⊢ 𝑟 = ( 0g ‘ 𝑑 )
39	35 10	cfv	⊢ ( 𝑒 ‘ 𝑟 )
40		clt	⊢ <
41	28 10	cfv	⊢ ( 𝑒 ‘ 𝑏 )
42	39 41 40	wbr	⊢ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 )
43	38 42	wo	⊢ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) )
44	37 43	wa	⊢ ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
45	44 26 12	wrex	⊢ ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
46	45 25 12	wrex	⊢ ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
47	46 24 16	wral	⊢ ∀ 𝑏 ∈ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
48	47 23 12	wral	⊢ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
49	11 22 48	w3a	⊢ ( Fun 𝑒 ∧ ( 𝑒 “ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) ⊆ ( 0 [,) +∞ ) ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) )
50	49 9 8	wsbc	⊢ [ ( Base ‘ 𝑑 ) / 𝑣 ] ( Fun 𝑒 ∧ ( 𝑒 “ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) ⊆ ( 0 [,) +∞ ) ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) )
51	50 6 5	wsbc	⊢ [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] ( Fun 𝑒 ∧ ( 𝑒 “ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) ⊆ ( 0 [,) +∞ ) ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) )
52	51 1 2	crab	⊢ { 𝑑 ∈ IDomn ∣ [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] ( Fun 𝑒 ∧ ( 𝑒 “ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) ⊆ ( 0 [,) +∞ ) ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) ) }
53	0 52	wceq	⊢ EDomn = { 𝑑 ∈ IDomn ∣ [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] ( Fun 𝑒 ∧ ( 𝑒 “ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) ⊆ ( 0 [,) +∞ ) ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) ) }