isedom

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

	Ref	Expression
Hypotheses	isedom.b	$⊢ B = {Base}_{D}$
	isedom.0	$⊢ \underset{˙}{0} = 0_{D}$
	isedom.p	$⊢ \underset{˙}{+} = +_{D}$
	isedom.m	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	isedom.e	$⊢ E = {EuclF (D) ↾}_{(B ∖ \{\underset{˙}{0}\})}$
Assertion	isedom	$⊢ D \in EDomn \leftrightarrow (D \in IDomn \land (E : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0} \land \forall x \in B \forall y \in (B ∖ \{\underset{˙}{0}\}) \exists q \in B \exists r \in B (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y)))))$

Proof

Step	Hyp	Ref	Expression
1		isedom.b	$⊢ B = {Base}_{D}$
2		isedom.0	$⊢ \underset{˙}{0} = 0_{D}$
3		isedom.p	$⊢ \underset{˙}{+} = +_{D}$
4		isedom.m	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
5		isedom.e	$⊢ E = {EuclF (D) ↾}_{(B ∖ \{\underset{˙}{0}\})}$
6		eqid	$⊢ EuclF (D) = EuclF (D)$
7		vex	$⊢ v \in V$
8	7	difexi	$⊢ v ∖ \{0_{d}\} \in V$
9	8	a1i	$⊢ (e = EuclF (D) \land v = B) \to v ∖ \{0_{d}\} \in V$
10		simpll	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to e = EuclF (D)$
11		simpr	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to w = v ∖ \{0_{d}\}$
12		simplr	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to v = B$
13	12	difeq1d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to v ∖ \{0_{d}\} = B ∖ \{0_{d}\}$
14	11 13	eqtrd	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to w = B ∖ \{0_{d}\}$
15	10 14	reseq12d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to {e ↾}_{w} = {EuclF (D) ↾}_{(B ∖ \{0_{d}\})}$
16	15 14	feq12d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to (({e ↾}_{w}) : w ⟶ ℕ_{0} \leftrightarrow ({EuclF (D) ↾}_{(B ∖ \{0_{d}\})}) : B ∖ \{0_{d}\} ⟶ ℕ_{0})$
17	10	fveq1d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to e (r) = EuclF (D) (r)$
18	10	fveq1d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to e (y) = EuclF (D) (y)$
19	17 18	breq12d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to (e (r) < e (y) \leftrightarrow EuclF (D) (r) < EuclF (D) (y))$
20	19	orbi2d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to ((r = 0_{d} \lor e (r) < e (y)) \leftrightarrow (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y)))$
21	20	anbi2d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to ((x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y))) \leftrightarrow (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))))$
22	12 21	rexeqbidv	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to (\exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y))) \leftrightarrow \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))))$
23	12 22	rexeqbidv	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to (\exists q \in v \exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y))) \leftrightarrow \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))))$
24	14 23	raleqbidv	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to (\forall y \in w \exists q \in v \exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y))) \leftrightarrow \forall y \in (B ∖ \{0_{d}\}) \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))))$
25	12 24	raleqbidv	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to (\forall x \in v \forall y \in w \exists q \in v \exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y))) \leftrightarrow \forall x \in B \forall y \in (B ∖ \{0_{d}\}) \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))))$
26	16 25	anbi12d	$⊢ ((e = EuclF (D) \land v = B) \land w = v ∖ \{0_{d}\}) \to ((({e ↾}_{w}) : w ⟶ ℕ_{0} \land \forall x \in v \forall y \in w \exists q \in v \exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y)))) \leftrightarrow (({EuclF (D) ↾}_{(B ∖ \{0_{d}\})}) : B ∖ \{0_{d}\} ⟶ ℕ_{0} \land \forall x \in B \forall y \in (B ∖ \{0_{d}\}) \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y)))))$
27	9 26	sbcied	$⊢ (e = EuclF (D) \land v = B) \to (\underset{˙}{[} (v ∖ \{0_{d}\}) / w \underset{˙}{]} (({e ↾}_{w}) : w ⟶ ℕ_{0} \land \forall x \in v \forall y \in w \exists q \in v \exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y)))) \leftrightarrow (({EuclF (D) ↾}_{(B ∖ \{0_{d}\})}) : B ∖ \{0_{d}\} ⟶ ℕ_{0} \land \forall x \in B \forall y \in (B ∖ \{0_{d}\}) \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y)))))$
28	6 1 27	sbcie2s	$⊢ d = D \to (\underset{˙}{[} EuclF (d) / e \underset{˙}{]} \underset{˙}{[} {Base}_{d} / v \underset{˙}{]} \underset{˙}{[} (v ∖ \{0_{d}\}) / w \underset{˙}{]} (({e ↾}_{w}) : w ⟶ ℕ_{0} \land \forall x \in v \forall y \in w \exists q \in v \exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y)))) \leftrightarrow (({EuclF (D) ↾}_{(B ∖ \{0_{d}\})}) : B ∖ \{0_{d}\} ⟶ ℕ_{0} \land \forall x \in B \forall y \in (B ∖ \{0_{d}\}) \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y)))))$
29		fveq2	$⊢ d = D \to 0_{d} = 0_{D}$
30	29 2	eqtr4di	$⊢ d = D \to 0_{d} = \underset{˙}{0}$
31	30	sneqd	$⊢ d = D \to \{0_{d}\} = \{\underset{˙}{0}\}$
32	31	difeq2d	$⊢ d = D \to B ∖ \{0_{d}\} = B ∖ \{\underset{˙}{0}\}$
33	32	reseq2d	$⊢ d = D \to {EuclF (D) ↾}_{(B ∖ \{0_{d}\})} = {EuclF (D) ↾}_{(B ∖ \{\underset{˙}{0}\})}$
34	33 5	eqtr4di	$⊢ d = D \to {EuclF (D) ↾}_{(B ∖ \{0_{d}\})} = E$
35	34 32	feq12d	$⊢ d = D \to (({EuclF (D) ↾}_{(B ∖ \{0_{d}\})}) : B ∖ \{0_{d}\} ⟶ ℕ_{0} \leftrightarrow E : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0})$
36		fveq2	$⊢ d = D \to +_{d} = +_{D}$
37	36 3	eqtr4di	$⊢ d = D \to +_{d} = \underset{˙}{+}$
38		fveq2	$⊢ d = D \to \cdot_{d} = \cdot_{D}$
39	38 4	eqtr4di	$⊢ d = D \to \cdot_{d} = \underset{˙}{\cdot}$
40	39	oveqd	$⊢ d = D \to y \cdot_{d} q = y \underset{˙}{\cdot} q$
41		eqidd	$⊢ d = D \to r = r$
42	37 40 41	oveq123d	$⊢ d = D \to (y \cdot_{d} q) +_{d} r = (y \underset{˙}{\cdot} q) \underset{˙}{+} r$
43	42	eqeq2d	$⊢ d = D \to (x = (y \cdot_{d} q) +_{d} r \leftrightarrow x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r)$
44	43	ad2antrr	$⊢ ((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \to (x = (y \cdot_{d} q) +_{d} r \leftrightarrow x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r)$
45	30	eqeq2d	$⊢ d = D \to (r = 0_{d} \leftrightarrow r = \underset{˙}{0})$
46	45	ad2antrr	$⊢ ((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \to (r = 0_{d} \leftrightarrow r = \underset{˙}{0})$
47	46	orbi1d	$⊢ ((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \to ((r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y)) \leftrightarrow (r = \underset{˙}{0} \lor EuclF (D) (r) < EuclF (D) (y)))$
48		biort	$⊢ r = \underset{˙}{0} \to (r = \underset{˙}{0} \leftrightarrow (r = \underset{˙}{0} \lor EuclF (D) (r) < EuclF (D) (y)))$
49		biort	$⊢ r = \underset{˙}{0} \to (r = \underset{˙}{0} \leftrightarrow (r = \underset{˙}{0} \lor E (r) < E (y)))$
50	48 49	bitr3d	$⊢ r = \underset{˙}{0} \to ((r = \underset{˙}{0} \lor EuclF (D) (r) < EuclF (D) (y)) \leftrightarrow (r = \underset{˙}{0} \lor E (r) < E (y)))$
51	50	adantl	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r = \underset{˙}{0}) \to ((r = \underset{˙}{0} \lor EuclF (D) (r) < EuclF (D) (y)) \leftrightarrow (r = \underset{˙}{0} \lor E (r) < E (y)))$
52	5	fveq1i	$⊢ E (r) = ({EuclF (D) ↾}_{(B ∖ \{\underset{˙}{0}\})}) (r)$
53		simplr	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to r \in B$
54		simpr	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to r \neq \underset{˙}{0}$
55	53 54	eldifsnd	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to r \in (B ∖ \{\underset{˙}{0}\})$
56	55	fvresd	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to ({EuclF (D) ↾}_{(B ∖ \{\underset{˙}{0}\})}) (r) = EuclF (D) (r)$
57	52 56	eqtr2id	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to EuclF (D) (r) = E (r)$
58	5	fveq1i	$⊢ E (y) = ({EuclF (D) ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y)$
59		simpr	$⊢ (d = D \land y \in (B ∖ \{0_{d}\})) \to y \in (B ∖ \{0_{d}\})$
60	32	adantr	$⊢ (d = D \land y \in (B ∖ \{0_{d}\})) \to B ∖ \{0_{d}\} = B ∖ \{\underset{˙}{0}\}$
61	59 60	eleqtrd	$⊢ (d = D \land y \in (B ∖ \{0_{d}\})) \to y \in (B ∖ \{\underset{˙}{0}\})$
62	61	ad2antrr	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to y \in (B ∖ \{\underset{˙}{0}\})$
63	62	fvresd	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to ({EuclF (D) ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y) = EuclF (D) (y)$
64	58 63	eqtr2id	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to EuclF (D) (y) = E (y)$
65	57 64	breq12d	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to (EuclF (D) (r) < EuclF (D) (y) \leftrightarrow E (r) < E (y))$
66	65	orbi2d	$⊢ (((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \land r \neq \underset{˙}{0}) \to ((r = \underset{˙}{0} \lor EuclF (D) (r) < EuclF (D) (y)) \leftrightarrow (r = \underset{˙}{0} \lor E (r) < E (y)))$
67	51 66	pm2.61dane	$⊢ ((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \to ((r = \underset{˙}{0} \lor EuclF (D) (r) < EuclF (D) (y)) \leftrightarrow (r = \underset{˙}{0} \lor E (r) < E (y)))$
68	47 67	bitrd	$⊢ ((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \to ((r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y)) \leftrightarrow (r = \underset{˙}{0} \lor E (r) < E (y)))$
69	44 68	anbi12d	$⊢ ((d = D \land y \in (B ∖ \{0_{d}\})) \land r \in B) \to ((x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))) \leftrightarrow (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y))))$
70	69	rexbidva	$⊢ (d = D \land y \in (B ∖ \{0_{d}\})) \to (\exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))) \leftrightarrow \exists r \in B (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y))))$
71	70	rexbidv	$⊢ (d = D \land y \in (B ∖ \{0_{d}\})) \to (\exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))) \leftrightarrow \exists q \in B \exists r \in B (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y))))$
72	32 71	raleqbidva	$⊢ d = D \to (\forall y \in (B ∖ \{0_{d}\}) \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))) \leftrightarrow \forall y \in (B ∖ \{\underset{˙}{0}\}) \exists q \in B \exists r \in B (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y))))$
73	72	ralbidv	$⊢ d = D \to (\forall x \in B \forall y \in (B ∖ \{0_{d}\}) \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y))) \leftrightarrow \forall x \in B \forall y \in (B ∖ \{\underset{˙}{0}\}) \exists q \in B \exists r \in B (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y))))$
74	35 73	anbi12d	$⊢ d = D \to ((({EuclF (D) ↾}_{(B ∖ \{0_{d}\})}) : B ∖ \{0_{d}\} ⟶ ℕ_{0} \land \forall x \in B \forall y \in (B ∖ \{0_{d}\}) \exists q \in B \exists r \in B (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor EuclF (D) (r) < EuclF (D) (y)))) \leftrightarrow (E : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0} \land \forall x \in B \forall y \in (B ∖ \{\underset{˙}{0}\}) \exists q \in B \exists r \in B (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y)))))$
75	28 74	bitrd	$⊢ d = D \to (\underset{˙}{[} EuclF (d) / e \underset{˙}{]} \underset{˙}{[} {Base}_{d} / v \underset{˙}{]} \underset{˙}{[} (v ∖ \{0_{d}\}) / w \underset{˙}{]} (({e ↾}_{w}) : w ⟶ ℕ_{0} \land \forall x \in v \forall y \in w \exists q \in v \exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y)))) \leftrightarrow (E : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0} \land \forall x \in B \forall y \in (B ∖ \{\underset{˙}{0}\}) \exists q \in B \exists r \in B (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y)))))$
76		df-edom	$⊢ EDomn = \{d \in IDomn \| \underset{˙}{[} EuclF (d) / e \underset{˙}{]} \underset{˙}{[} {Base}_{d} / v \underset{˙}{]} \underset{˙}{[} (v ∖ \{0_{d}\}) / w \underset{˙}{]} (({e ↾}_{w}) : w ⟶ ℕ_{0} \land \forall x \in v \forall y \in w \exists q \in v \exists r \in v (x = (y \cdot_{d} q) +_{d} r \land (r = 0_{d} \lor e (r) < e (y))))\}$
77	75 76	elrab2	$⊢ D \in EDomn \leftrightarrow (D \in IDomn \land (E : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0} \land \forall x \in B \forall y \in (B ∖ \{\underset{˙}{0}\}) \exists q \in B \exists r \in B (x = (y \underset{˙}{\cdot} q) \underset{˙}{+} r \land (r = \underset{˙}{0} \lor E (r) < E (y)))))$

Metamath Proof Explorer

Theorem isedom

Proof