Definition df-edom

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

	Ref	Expression
Assertion	df-edom	⊢ EDomn = { 𝑑 ∈ IDomn ∣ [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .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	9	cv	⊢ 𝑣
11		c0g	⊢ 0g
12	4 11	cfv	⊢ ( 0g ‘ 𝑑 )
13	12	csn	⊢ { ( 0g ‘ 𝑑 ) }
14	10 13	cdif	⊢ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } )
15		vw	⊢ 𝑤
16	6	cv	⊢ 𝑒
17	15	cv	⊢ 𝑤
18	16 17	cres	⊢ ( 𝑒 ↾ 𝑤 )
19		cn0	⊢ ℕ0
20	17 19 18	wf	⊢ ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0
21		va	⊢ 𝑎
22		vb	⊢ 𝑏
23		vq	⊢ 𝑞
24		vr	⊢ 𝑟
25	21	cv	⊢ 𝑎
26	22	cv	⊢ 𝑏
27		cmulr	⊢ .r
28	4 27	cfv	⊢ ( .r ‘ 𝑑 )
29	23	cv	⊢ 𝑞
30	26 29 28	co	⊢ ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 )
31		cplusg	⊢ +g
32	4 31	cfv	⊢ ( +g ‘ 𝑑 )
33	24	cv	⊢ 𝑟
34	30 33 32	co	⊢ ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 )
35	25 34	wceq	⊢ 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 )
36	33 12	wceq	⊢ 𝑟 = ( 0g ‘ 𝑑 )
37	33 16	cfv	⊢ ( 𝑒 ‘ 𝑟 )
38		clt	⊢ <
39	26 16	cfv	⊢ ( 𝑒 ‘ 𝑏 )
40	37 39 38	wbr	⊢ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 )
41	36 40	wo	⊢ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) )
42	35 41	wa	⊢ ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
43	42 24 10	wrex	⊢ ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
44	43 23 10	wrex	⊢ ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
45	44 22 17	wral	⊢ ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
46	45 21 10	wral	⊢ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) )
47	20 46	wa	⊢ ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) )
48	47 15 14	wsbc	⊢ [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) )
49	48 9 8	wsbc	⊢ [ ( Base ‘ 𝑑 ) / 𝑣 ] [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) )
50	49 6 5	wsbc	⊢ [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) )
51	50 1 2	crab	⊢ { 𝑑 ∈ IDomn ∣ [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) ) }
52	0 51	wceq	⊢ EDomn = { 𝑑 ∈ IDomn ∣ [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑎 = ( ( 𝑏 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑏 ) ) ) ) }