Metamath Proof Explorer

Theorem isedom

Description: Property of being a Euclidean domain. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses isedom.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
isedom.0 ⊢ 0 = ( 0g ‘ 𝐷 )
isedom.p ⊢ + = ( +g ‘ 𝐷 )
isedom.m ⊢ · = ( .r ‘ 𝐷 )
isedom.e ⊢ 𝐸 = ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) )
Assertion isedom ( 𝐷 ∈ EDomn ↔ ( 𝐷 ∈ IDomn ∧ ( 𝐸 : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isedom.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 isedom.0 ⊢ 0 = ( 0g ‘ 𝐷 )
3 isedom.p ⊢ + = ( +g ‘ 𝐷 )
4 isedom.m ⊢ · = ( .r ‘ 𝐷 )
5 isedom.e ⊢ 𝐸 = ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) )
6 eqid ⊢ ( EuclF ‘ 𝐷 ) = ( EuclF ‘ 𝐷 )
7 vex ⊢ 𝑣 ∈ V
8 7 difexi ⊢ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∈ V
9 8 a1i ⊢ ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) → ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ∈ V )
10 simpll ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → 𝑒 = ( EuclF ‘ 𝐷 ) )
11 simpr ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) )
12 simplr ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → 𝑣 = 𝐵 )
13 12 difeq1d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) = ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) )
14 11 13 eqtrd ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → 𝑤 = ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) )
15 10 14 reseq12d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( 𝑒 ↾ 𝑤 ) = ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) )
16 15 14 feq12d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ↔ ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) : ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ⟶ ℕ0 ) )
17 10 fveq1d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( 𝑒 ‘ 𝑟 ) = ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) )
18 10 fveq1d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( 𝑒 ‘ 𝑦 ) = ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) )
19 17 18 breq12d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ↔ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) )
20 19 orbi2d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ↔ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) )
21 20 anbi2d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ↔ ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) )
22 12 21 rexeqbidv ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) )
23 12 22 rexeqbidv ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ↔ ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) )
24 14 23 raleqbidv ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ∀ 𝑦 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) )
25 12 24 raleqbidv ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) )
26 16 25 anbi12d ⊢ ( ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) ∧ 𝑤 = ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ) ↔ ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) : ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) ) )
27 9 26 sbcied ⊢ ( ( 𝑒 = ( EuclF ‘ 𝐷 ) ∧ 𝑣 = 𝐵 ) → ( [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ) ↔ ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) : ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) ) )
28 6 1 27 sbcie2s ⊢ ( 𝑑 = 𝐷 → ( [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ) ↔ ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) : ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) ) )
29 fveq2 ⊢ ( 𝑑 = 𝐷 → ( 0g ‘ 𝑑 ) = ( 0g ‘ 𝐷 ) )
30 29 2 eqtr4di ⊢ ( 𝑑 = 𝐷 → ( 0g ‘ 𝑑 ) = 0 )
31 30 sneqd ⊢ ( 𝑑 = 𝐷 → { ( 0g ‘ 𝑑 ) } = { 0 } )
32 31 difeq2d ⊢ ( 𝑑 = 𝐷 → ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) = ( 𝐵 ∖ { 0 } ) )
33 32 reseq2d ⊢ ( 𝑑 = 𝐷 → ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) = ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) ) )
34 33 5 eqtr4di ⊢ ( 𝑑 = 𝐷 → ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) = 𝐸 )
35 34 32 feq12d ⊢ ( 𝑑 = 𝐷 → ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) : ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ⟶ ℕ0 ↔ 𝐸 : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ) )
36 fveq2 ⊢ ( 𝑑 = 𝐷 → ( +g ‘ 𝑑 ) = ( +g ‘ 𝐷 ) )
37 36 3 eqtr4di ⊢ ( 𝑑 = 𝐷 → ( +g ‘ 𝑑 ) = + )
38 fveq2 ⊢ ( 𝑑 = 𝐷 → ( .r ‘ 𝑑 ) = ( .r ‘ 𝐷 ) )
39 38 4 eqtr4di ⊢ ( 𝑑 = 𝐷 → ( .r ‘ 𝑑 ) = · )
40 39 oveqd ⊢ ( 𝑑 = 𝐷 → ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) = ( 𝑦 · 𝑞 ) )
41 eqidd ⊢ ( 𝑑 = 𝐷 → 𝑟 = 𝑟 )
42 37 40 41 oveq123d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) = ( ( 𝑦 · 𝑞 ) + 𝑟 ) )
43 42 eqeq2d ⊢ ( 𝑑 = 𝐷 → ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ↔ 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ) )
44 43 ad2antrr ⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) → ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ↔ 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ) )
45 30 eqeq2d ⊢ ( 𝑑 = 𝐷 → ( 𝑟 = ( 0g ‘ 𝑑 ) ↔ 𝑟 = 0 ) )
46 45 ad2antrr ⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) → ( 𝑟 = ( 0g ‘ 𝑑 ) ↔ 𝑟 = 0 ) )
47 46 orbi1d ⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ↔ ( 𝑟 = 0 ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) )
48 biort ⊢ ( 𝑟 = 0 → ( 𝑟 = 0 ↔ ( 𝑟 = 0 ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) )
49 biort ⊢ ( 𝑟 = 0 → ( 𝑟 = 0 ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) )
50 48 49 bitr3d ⊢ ( 𝑟 = 0 → ( ( 𝑟 = 0 ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) )
51 50 adantl ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 = 0 ) → ( ( 𝑟 = 0 ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) )
52 5 fveq1i ⊢ ( 𝐸 ‘ 𝑟 ) = ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 )
53 simplr ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ 𝐵 )
54 simpr ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → 𝑟 ≠ 0 )
55 53 54 eldifsnd ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ ( 𝐵 ∖ { 0 } ) )
56 55 fvresd ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) = ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) )
57 52 56 eqtr2id ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) = ( 𝐸 ‘ 𝑟 ) )
58 5 fveq1i ⊢ ( 𝐸 ‘ 𝑦 ) = ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 )
59 simpr ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) → 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) )
60 32 adantr ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) = ( 𝐵 ∖ { 0 } ) )
61 59 60 eleqtrd ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) → 𝑦 ∈ ( 𝐵 ∖ { 0 } ) )
62 61 ad2antrr ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → 𝑦 ∈ ( 𝐵 ∖ { 0 } ) )
63 62 fvresd ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) = ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) )
64 58 63 eqtr2id ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) = ( 𝐸 ‘ 𝑦 ) )
65 57 64 breq12d ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ↔ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) )
66 65 orbi2d ⊢ ( ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( 𝑟 = 0 ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) )
67 51 66 pm2.61dane ⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑟 = 0 ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) )
68 47 67 bitrd ⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) )
69 44 68 anbi12d ⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ↔ ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) )
70 69 rexbidva ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) )
71 70 rexbidv ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) → ( ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ↔ ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) )
72 32 71 raleqbidva ⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) )
73 72 ralbidv ⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) )
74 35 73 anbi12d ⊢ ( 𝑑 = 𝐷 → ( ( ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ) : ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑑 ) } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( ( EuclF ‘ 𝐷 ) ‘ 𝑟 ) < ( ( EuclF ‘ 𝐷 ) ‘ 𝑦 ) ) ) ) ↔ ( 𝐸 : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) ) )
75 28 74 bitrd ⊢ ( 𝑑 = 𝐷 → ( [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ) ↔ ( 𝐸 : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) ) )
76 df-edom ⊢ EDomn = { 𝑑 ∈ IDomn ∣ [ ( EuclF ‘ 𝑑 ) / 𝑒 ] [ ( Base ‘ 𝑑 ) / 𝑣 ] [ ( 𝑣 ∖ { ( 0g ‘ 𝑑 ) } ) / 𝑤 ] ( ( 𝑒 ↾ 𝑤 ) : 𝑤 ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑤 ∃ 𝑞 ∈ 𝑣 ∃ 𝑟 ∈ 𝑣 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝑑 ) 𝑞 ) ( +g ‘ 𝑑 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝑑 ) ∨ ( 𝑒 ‘ 𝑟 ) < ( 𝑒 ‘ 𝑦 ) ) ) ) }
77 75 76 elrab2 ⊢ ( 𝐷 ∈ EDomn ↔ ( 𝐷 ∈ IDomn ∧ ( 𝐸 : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑦 ) ) ) ) ) )