Theorem isedom 33934

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

Hypotheses

Ref	Expression
isedom.b	⊢ 𝐵 = (Base‘𝐷)
isedom.0	⊢ 0 = (0g‘𝐷)
isedom.p	⊢ + = (+g‘𝐷)
isedom.m	⊢ · = (.r‘𝐷)
isedom.e	⊢ 𝐸 = ((EuclF‘𝐷) ↾ (𝐵 ∖ { 0 }))

Assertion

Ref	Expression
isedom	⊢ (𝐷 ∈ EDomn ↔ (𝐷 ∈ IDomn ∧ (𝐸:(𝐵 ∖ { 0 })⟶ℕ0 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ { 0 })∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))))

Distinct variable groups:   𝑦, 0   𝐵,𝑞,𝑟,𝑥,𝑦   𝐷,𝑞,𝑟,𝑥,𝑦   𝐸,𝑞,𝑟,𝑥,𝑦

Allowed substitution hints:   + (𝑥, 𝑦, 𝑟, 𝑞)   · (𝑥, 𝑦, 𝑟, 𝑞)   0 (𝑥, 𝑟, 𝑞)

Proof of Theorem isedom

Dummy variables 𝑑 𝑒 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2763	. . . 4 ⊢ (EuclF‘𝐷) = (EuclF‘𝐷)
2		isedom.b	. . . 4 ⊢ 𝐵 = (Base‘𝐷)
3		vex 3458	. . . . . . 7 ⊢ 𝑣 ∈ V
4	3	difexi 5297	. . . . . 6 ⊢ (𝑣 ∖ {(0g‘𝑑)}) ∈ V
5	4	a1i 11	. . . . 5 ⊢ ((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) → (𝑣 ∖ {(0g‘𝑑)}) ∈ V)
6		simpll 779	. . . . . . . 8 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → 𝑒 = (EuclF‘𝐷))
7		simpr 490	. . . . . . . . 9 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → 𝑤 = (𝑣 ∖ {(0g‘𝑑)}))
8		simplr 781	. . . . . . . . . 10 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → 𝑣 = 𝐵)
9	8	difeq1d 4065	. . . . . . . . 9 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (𝑣 ∖ {(0g‘𝑑)}) = (𝐵 ∖ {(0g‘𝑑)}))
10	7, 9	eqtrd 2798	. . . . . . . 8 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → 𝑤 = (𝐵 ∖ {(0g‘𝑑)}))
11	6, 10	reseq12d 5983	. . . . . . 7 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (𝑒 ↾ 𝑤) = ((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})))
12	11, 10	feq12d 6722	. . . . . 6 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → ((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ↔ ((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})):(𝐵 ∖ {(0g‘𝑑)})⟶ℕ0))
13	6	fveq1d 6913	. . . . . . . . . . . . 13 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (𝑒‘𝑟) = ((EuclF‘𝐷)‘𝑟))
14	6	fveq1d 6913	. . . . . . . . . . . . 13 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (𝑒‘𝑦) = ((EuclF‘𝐷)‘𝑦))
15	13, 14	breq12d 5119	. . . . . . . . . . . 12 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → ((𝑒‘𝑟) < (𝑒‘𝑦) ↔ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)))
16	15	orbi2d 929	. . . . . . . . . . 11 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → ((𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦)) ↔ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))))
17	16	anbi2d 642	. . . . . . . . . 10 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → ((𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦))) ↔ (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)))))
18	8, 17	rexeqbidv 3339	. . . . . . . . 9 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦))) ↔ ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)))))
19	8, 18	rexeqbidv 3339	. . . . . . . 8 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦))) ↔ ∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)))))
20	10, 19	raleqbidv 3338	. . . . . . 7 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (∀𝑦 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦))) ↔ ∀𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)))))
21	8, 20	raleqbidv 3338	. . . . . 6 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)))))
22	12, 21	anbi12d 644	. . . . 5 ⊢ (((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) ∧ 𝑤 = (𝑣 ∖ {(0g‘𝑑)})) → (((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦)))) ↔ (((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})):(𝐵 ∖ {(0g‘𝑑)})⟶ℕ0 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))))))
23	5, 22	sbcied 3785	. . . 4 ⊢ ((𝑒 = (EuclF‘𝐷) ∧ 𝑣 = 𝐵) → ([(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦)))) ↔ (((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})):(𝐵 ∖ {(0g‘𝑑)})⟶ℕ0 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))))))
24	1, 2, 23	sbcie2s 17371	. . 3 ⊢ (𝑑 = 𝐷 → ([(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣][(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦)))) ↔ (((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})):(𝐵 ∖ {(0g‘𝑑)})⟶ℕ0 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))))))
25		fveq2 6911	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → (0g‘𝑑) = (0g‘𝐷))
26		isedom.0	. . . . . . . . . 10 ⊢ 0 = (0g‘𝐷)
27	25, 26	eqtr4di 2816	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (0g‘𝑑) = 0 )
28	27	sneqd 4596	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → {(0g‘𝑑)} = { 0 })
29	28	difeq2d 4066	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (𝐵 ∖ {(0g‘𝑑)}) = (𝐵 ∖ { 0 }))
30	29	reseq2d 5982	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})) = ((EuclF‘𝐷) ↾ (𝐵 ∖ { 0 })))
31		isedom.e	. . . . . 6 ⊢ 𝐸 = ((EuclF‘𝐷) ↾ (𝐵 ∖ { 0 }))
32	30, 31	eqtr4di 2816	. . . . 5 ⊢ (𝑑 = 𝐷 → ((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})) = 𝐸)
33	32, 29	feq12d 6722	. . . 4 ⊢ (𝑑 = 𝐷 → (((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})):(𝐵 ∖ {(0g‘𝑑)})⟶ℕ0 ↔ 𝐸:(𝐵 ∖ { 0 })⟶ℕ0))
34		fveq2 6911	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝐷 → (+g‘𝑑) = (+g‘𝐷))
35		isedom.p	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝐷)
36	34, 35	eqtr4di 2816	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → (+g‘𝑑) = + )
37		fveq2 6911	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝐷 → (.r‘𝑑) = (.r‘𝐷))
38		isedom.m	. . . . . . . . . . . . . 14 ⊢ · = (.r‘𝐷)
39	37, 38	eqtr4di 2816	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝐷 → (.r‘𝑑) = · )
40	39	oveqd 7463	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → (𝑦(.r‘𝑑)𝑞) = (𝑦 · 𝑞))
41		eqidd 2764	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → 𝑟 = 𝑟)
42	36, 40, 41	oveq123d 7467	. . . . . . . . . . 11 ⊢ (𝑑 = 𝐷 → ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) = ((𝑦 · 𝑞) + 𝑟))
43	42	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ↔ 𝑥 = ((𝑦 · 𝑞) + 𝑟)))
44	43	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) → (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ↔ 𝑥 = ((𝑦 · 𝑞) + 𝑟)))
45	27	eqeq2d 2774	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → (𝑟 = (0g‘𝑑) ↔ 𝑟 = 0 ))
46	45	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) → (𝑟 = (0g‘𝑑) ↔ 𝑟 = 0 ))
47	46	orbi1d 930	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) → ((𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)) ↔ (𝑟 = 0 ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))))
48		biort 949	. . . . . . . . . . . . 13 ⊢ (𝑟 = 0 → (𝑟 = 0 ↔ (𝑟 = 0 ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))))
49		biort 949	. . . . . . . . . . . . 13 ⊢ (𝑟 = 0 → (𝑟 = 0 ↔ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))
50	48, 49	bitr3d 284	. . . . . . . . . . . 12 ⊢ (𝑟 = 0 → ((𝑟 = 0 ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)) ↔ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))
51	50	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 = 0 ) → ((𝑟 = 0 ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)) ↔ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))
52	31	fveq1i 6912	. . . . . . . . . . . . . 14 ⊢ (𝐸‘𝑟) = (((EuclF‘𝐷) ↾ (𝐵 ∖ { 0 }))‘𝑟)
53		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ 𝐵)
54		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → 𝑟 ≠ 0 )
55	53, 54	eldifsnd 4750	. . . . . . . . . . . . . . 15 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ (𝐵 ∖ { 0 }))
56	55	fvresd 6931	. . . . . . . . . . . . . 14 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → (((EuclF‘𝐷) ↾ (𝐵 ∖ { 0 }))‘𝑟) = ((EuclF‘𝐷)‘𝑟))
57	52, 56	eqtr2id 2811	. . . . . . . . . . . . 13 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → ((EuclF‘𝐷)‘𝑟) = (𝐸‘𝑟))
58	31	fveq1i 6912	. . . . . . . . . . . . . 14 ⊢ (𝐸‘𝑦) = (((EuclF‘𝐷) ↾ (𝐵 ∖ { 0 }))‘𝑦)
59		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) → 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)}))
60	29	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) → (𝐵 ∖ {(0g‘𝑑)}) = (𝐵 ∖ { 0 }))
61	59, 60	eleqtrd 2866	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) → 𝑦 ∈ (𝐵 ∖ { 0 }))
62	61	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → 𝑦 ∈ (𝐵 ∖ { 0 }))
63	62	fvresd 6931	. . . . . . . . . . . . . 14 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → (((EuclF‘𝐷) ↾ (𝐵 ∖ { 0 }))‘𝑦) = ((EuclF‘𝐷)‘𝑦))
64	58, 63	eqtr2id 2811	. . . . . . . . . . . . 13 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → ((EuclF‘𝐷)‘𝑦) = (𝐸‘𝑦))
65	57, 64	breq12d 5119	. . . . . . . . . . . 12 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → (((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦) ↔ (𝐸‘𝑟) < (𝐸‘𝑦)))
66	65	orbi2d 929	. . . . . . . . . . 11 ⊢ ((((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) ∧ 𝑟 ≠ 0 ) → ((𝑟 = 0 ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)) ↔ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))
67	51, 66	pm2.61dane 3046	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) → ((𝑟 = 0 ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)) ↔ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))
68	47, 67	bitrd 282	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) → ((𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)) ↔ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))
69	44, 68	anbi12d 644	. . . . . . . 8 ⊢ (((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) ∧ 𝑟 ∈ 𝐵) → ((𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))) ↔ (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦)))))
70	69	rexbidva 3188	. . . . . . 7 ⊢ ((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) → (∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))) ↔ ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦)))))
71	70	rexbidv 3190	. . . . . 6 ⊢ ((𝑑 = 𝐷 ∧ 𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})) → (∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))) ↔ ∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦)))))
72	29, 71	raleqbidva 3329	. . . . 5 ⊢ (𝑑 = 𝐷 → (∀𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))) ↔ ∀𝑦 ∈ (𝐵 ∖ { 0 })∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦)))))
73	72	ralbidv 3189	. . . 4 ⊢ (𝑑 = 𝐷 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ { 0 })∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦)))))
74	33, 73	anbi12d 644	. . 3 ⊢ (𝑑 = 𝐷 → ((((EuclF‘𝐷) ↾ (𝐵 ∖ {(0g‘𝑑)})):(𝐵 ∖ {(0g‘𝑑)})⟶ℕ0 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ ((EuclF‘𝐷)‘𝑟) < ((EuclF‘𝐷)‘𝑦)))) ↔ (𝐸:(𝐵 ∖ { 0 })⟶ℕ0 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ { 0 })∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))))
75	24, 74	bitrd 282	. 2 ⊢ (𝑑 = 𝐷 → ([(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣][(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦)))) ↔ (𝐸:(𝐵 ∖ { 0 })⟶ℕ0 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ { 0 })∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))))
76		df-edom 33933	. 2 ⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣][(𝑣 ∖ {(0g‘𝑑)}) / 𝑤]((𝑒 ↾ 𝑤):𝑤⟶ℕ0 ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑤 ∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑥 = ((𝑦(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑦))))}
77	75, 76	elrab2 3652	1 ⊢ (𝐷 ∈ EDomn ↔ (𝐷 ∈ IDomn ∧ (𝐸:(𝐵 ∖ { 0 })⟶ℕ0 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ { 0 })∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦 · 𝑞) + 𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑦))))))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  Vcvv 3454  [wsbc 3742   ∖ cdif 4048  {csn 4588   class class class wbr 5106   ↾ cres 5658  ⟶wf 6557  ‘cfv 6561  (class class class)co 7446   < clt 11373  ℕ₀cn0 12636  Basecbs 17419  +_gcplusg 17460  ._rcmulr 17461  0_gc0g 17642  IDomncidom 20978  EuclFceuf 33928  EDomncedom 33932

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7449  df-edom 33933

This theorem is used by:  edomidom  33935  edomediv  33936  fldedom  33937  zzedom  33939  edompidlem  33940