edompidlem

Description: Lemma for edompid : In a Euclidean domain, all (non-zero) ideals are generated by a single element. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Hypotheses	edompidlem.b	$⊢ B = {Base}_{D}$
	edompidlem.o	$⊢ \underset{˙}{0} = 0_{D}$
	edompidlem.k	$⊢ K = RSpan (D)$
	edompidlem.e	$⊢ E = EuclF (D)$
	edompidlem.m	$⊢ M = inf (E [I ∖ \{\underset{˙}{0}\}] ℕ_{0} <)$
	edompidlem.d	$⊢ φ \to D \in EDomn$
	edompidlem.i	$⊢ φ \to I \in LIdeal (D)$
	edompidlem.1	$⊢ φ \to I \neq \{\underset{˙}{0}\}$
Assertion	edompidlem	$⊢ φ \to \exists g \in B I = K (\{g\})$

Proof

Step	Hyp	Ref	Expression
1		edompidlem.b	$⊢ B = {Base}_{D}$
2		edompidlem.o	$⊢ \underset{˙}{0} = 0_{D}$
3		edompidlem.k	$⊢ K = RSpan (D)$
4		edompidlem.e	$⊢ E = EuclF (D)$
5		edompidlem.m	$⊢ M = inf (E [I ∖ \{\underset{˙}{0}\}] ℕ_{0} <)$
6		edompidlem.d	$⊢ φ \to D \in EDomn$
7		edompidlem.i	$⊢ φ \to I \in LIdeal (D)$
8		edompidlem.1	$⊢ φ \to I \neq \{\underset{˙}{0}\}$
9		eqid	$⊢ LIdeal (D) = LIdeal (D)$
10	1 9	lidlss	$⊢ I \in LIdeal (D) \to I \subseteq B$
11	7 10	syl	$⊢ φ \to I \subseteq B$
12	11	ssdifssd	$⊢ φ \to I ∖ \{\underset{˙}{0}\} \subseteq B$
13		simplr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to a = (g \cdot_{D} q) +_{D} r$
14		simpr	$⊢ ((((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \land r = \underset{˙}{0}) \to r = \underset{˙}{0}$
15		ltrel	$⊢ Rel <$
16	15	a1i	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to Rel <$
17		ltwenn0	$⊢ < We ℕ_{0}$
18	17	a1i	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to < We ℕ_{0}$
19	4	fvexi	$⊢ E \in V$
20	19	a1i	$⊢ φ \to E \in V$
21	20	imaexd	$⊢ φ \to E [I ∖ \{\underset{˙}{0}\}] \in V$
22	21	ad7antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to E [I ∖ \{\underset{˙}{0}\}] \in V$
23	11	ssdifd	$⊢ φ \to I ∖ \{\underset{˙}{0}\} \subseteq B ∖ \{\underset{˙}{0}\}$
24		imass2	$⊢ I ∖ \{\underset{˙}{0}\} \subseteq B ∖ \{\underset{˙}{0}\} \to E [I ∖ \{\underset{˙}{0}\}] \subseteq E [B ∖ \{\underset{˙}{0}\}]$
25	23 24	syl	$⊢ φ \to E [I ∖ \{\underset{˙}{0}\}] \subseteq E [B ∖ \{\underset{˙}{0}\}]$
26		resima	$⊢ ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [B ∖ \{\underset{˙}{0}\}] = E [B ∖ \{\underset{˙}{0}\}]$
27		eqid	$⊢ +_{D} = +_{D}$
28		eqid	$⊢ \cdot_{D} = \cdot_{D}$
29	4	reseq1i	$⊢ {E ↾}_{(B ∖ \{\underset{˙}{0}\})} = {EuclF (D) ↾}_{(B ∖ \{\underset{˙}{0}\})}$
30	1 2 27 28 29	isedom	$⊢ D \in EDomn \leftrightarrow (D \in IDomn \land (({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) : 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 \cdot_{D} q) +_{D} r \land (r = \underset{˙}{0} \lor ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (r) < ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y)))))$
31	6 30	sylib	$⊢ φ \to (D \in IDomn \land (({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) : 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 \cdot_{D} q) +_{D} r \land (r = \underset{˙}{0} \lor ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (r) < ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y)))))$
32	31	simprld	$⊢ φ \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0}$
33	32	fimassd	$⊢ φ \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [B ∖ \{\underset{˙}{0}\}] \subseteq ℕ_{0}$
34	26 33	eqsstrrid	$⊢ φ \to E [B ∖ \{\underset{˙}{0}\}] \subseteq ℕ_{0}$
35	25 34	sstrd	$⊢ φ \to E [I ∖ \{\underset{˙}{0}\}] \subseteq ℕ_{0}$
36	35	ad7antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to E [I ∖ \{\underset{˙}{0}\}] \subseteq ℕ_{0}$
37	31	simpld	$⊢ φ \to D \in IDomn$
38	37	idomringd	$⊢ φ \to D \in Ring$
39	9 2	lidl0cl	$⊢ (D \in Ring \land I \in LIdeal (D)) \to \underset{˙}{0} \in I$
40	38 7 39	syl2anc	$⊢ φ \to \underset{˙}{0} \in I$
41	40	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq I$
42	8	necomd	$⊢ φ \to \{\underset{˙}{0}\} \neq I$
43		pssdifn0	$⊢ (\{\underset{˙}{0}\} \subseteq I \land \{\underset{˙}{0}\} \neq I) \to I ∖ \{\underset{˙}{0}\} \neq \emptyset$
44	41 42 43	syl2anc	$⊢ φ \to I ∖ \{\underset{˙}{0}\} \neq \emptyset$
45	32	ffnd	$⊢ φ \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) Fn (B ∖ \{\underset{˙}{0}\})$
46	45	adantr	$⊢ (φ \land x \in (I ∖ \{\underset{˙}{0}\})) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) Fn (B ∖ \{\underset{˙}{0}\})$
47	23	sselda	$⊢ (φ \land x \in (I ∖ \{\underset{˙}{0}\})) \to x \in (B ∖ \{\underset{˙}{0}\})$
48		simpr	$⊢ (φ \land x \in (I ∖ \{\underset{˙}{0}\})) \to x \in (I ∖ \{\underset{˙}{0}\})$
49	46 47 48	fnfvimad	$⊢ (φ \land x \in (I ∖ \{\underset{˙}{0}\})) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) \in ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [I ∖ \{\underset{˙}{0}\}]$
50		resima2	$⊢ I ∖ \{\underset{˙}{0}\} \subseteq B ∖ \{\underset{˙}{0}\} \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [I ∖ \{\underset{˙}{0}\}] = E [I ∖ \{\underset{˙}{0}\}]$
51	23 50	syl	$⊢ φ \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [I ∖ \{\underset{˙}{0}\}] = E [I ∖ \{\underset{˙}{0}\}]$
52	51	adantr	$⊢ (φ \land x \in (I ∖ \{\underset{˙}{0}\})) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [I ∖ \{\underset{˙}{0}\}] = E [I ∖ \{\underset{˙}{0}\}]$
53	49 52	eleqtrd	$⊢ (φ \land x \in (I ∖ \{\underset{˙}{0}\})) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) \in E [I ∖ \{\underset{˙}{0}\}]$
54	53	ne0d	$⊢ (φ \land x \in (I ∖ \{\underset{˙}{0}\})) \to E [I ∖ \{\underset{˙}{0}\}] \neq \emptyset$
55	44 54	n0limd	$⊢ φ \to E [I ∖ \{\underset{˙}{0}\}] \neq \emptyset$
56	55	ad7antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to E [I ∖ \{\underset{˙}{0}\}] \neq \emptyset$
57	45	ad7antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) Fn (B ∖ \{\underset{˙}{0}\})$
58		simpllr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to r \in B$
59		simpr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to r \neq \underset{˙}{0}$
60	58 59	eldifsnd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to r \in (B ∖ \{\underset{˙}{0}\})$
61		simplr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to a = (g \cdot_{D} q) +_{D} r$
62	61	oveq1d	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to a -_{D} (g \cdot_{D} q) = ((g \cdot_{D} q) +_{D} r) -_{D} (g \cdot_{D} q)$
63	38	ringabld	$⊢ φ \to D \in Abel$
64	63	ad7antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to D \in Abel$
65	38	ad2antrr	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to D \in Ring$
66	65	ad5antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to D \in Ring$
67	23	sselda	$⊢ (φ \land g \in (I ∖ \{\underset{˙}{0}\})) \to g \in (B ∖ \{\underset{˙}{0}\})$
68	67	eldifad	$⊢ (φ \land g \in (I ∖ \{\underset{˙}{0}\})) \to g \in B$
69	68	ad6antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to g \in B$
70		simp-4r	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to q \in B$
71	1 28 66 69 70	ringcld	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to g \cdot_{D} q \in B$
72		eqid	$⊢ -_{D} = -_{D}$
73	1 27 72	ablpncan2	$⊢ (D \in Abel \land g \cdot_{D} q \in B \land r \in B) \to ((g \cdot_{D} q) +_{D} r) -_{D} (g \cdot_{D} q) = r$
74	64 71 58 73	syl3anc	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to ((g \cdot_{D} q) +_{D} r) -_{D} (g \cdot_{D} q) = r$
75	62 74	eqtr2d	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to r = a -_{D} (g \cdot_{D} q)$
76	7	ad2antrr	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to I \in LIdeal (D)$
77	76	ad5antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to I \in LIdeal (D)$
78		simp-5r	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to a \in I$
79	37	idomcringd	$⊢ φ \to D \in CRing$
80	79	ad6antr	$⊢ ((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \to D \in CRing$
81		simpllr	$⊢ ((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \to q \in B$
82	68	ad5antr	$⊢ ((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \to g \in B$
83	1 28 80 81 82	crngcomd	$⊢ ((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \to q \cdot_{D} g = g \cdot_{D} q$
84	83	adantr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to q \cdot_{D} g = g \cdot_{D} q$
85		simplr	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to g \in (I ∖ \{\underset{˙}{0}\})$
86	85	eldifad	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to g \in I$
87	86	ad5antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to g \in I$
88	9 1 28 66 77 70 87	lidlmcld	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to q \cdot_{D} g \in I$
89	84 88	eqeltrrd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to g \cdot_{D} q \in I$
90	9 72	lidlsubcl	$⊢ ((D \in Ring \land I \in LIdeal (D)) \land (a \in I \land g \cdot_{D} q \in I)) \to a -_{D} (g \cdot_{D} q) \in I$
91	66 77 78 89 90	syl22anc	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to a -_{D} (g \cdot_{D} q) \in I$
92	75 91	eqeltrd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to r \in I$
93	92 59	eldifsnd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to r \in (I ∖ \{\underset{˙}{0}\})$
94	57 60 93	fnfvimad	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (r) \in ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [I ∖ \{\underset{˙}{0}\}]$
95	60	fvresd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (r) = E (r)$
96	51	ad7antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [I ∖ \{\underset{˙}{0}\}] = E [I ∖ \{\underset{˙}{0}\}]$
97	94 95 96	3eltr3d	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to E (r) \in E [I ∖ \{\underset{˙}{0}\}]$
98	16 18 22 36 56 97	weinflb	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to \neg E (r) < inf (E [I ∖ \{\underset{˙}{0}\}] ℕ_{0} <)$
99		simp-6r	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M$
100	67	ad2antrr	$⊢ (((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \to g \in (B ∖ \{\underset{˙}{0}\})$
101	100	fvresd	$⊢ (((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = E (g)$
102	101	ad4antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = E (g)$
103	5	a1i	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to M = inf (E [I ∖ \{\underset{˙}{0}\}] ℕ_{0} <)$
104	99 102 103	3eqtr3rd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to inf (E [I ∖ \{\underset{˙}{0}\}] ℕ_{0} <) = E (g)$
105	98 104	brneqtrd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land r \neq \underset{˙}{0}) \to \neg E (r) < E (g)$
106	105	ex	$⊢ ((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \to (r \neq \underset{˙}{0} \to \neg E (r) < E (g))$
107	106	adantr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to (r \neq \underset{˙}{0} \to \neg E (r) < E (g))$
108	107	necon4ad	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to (E (r) < E (g) \to r = \underset{˙}{0})$
109	108	imp	$⊢ ((((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \land E (r) < E (g)) \to r = \underset{˙}{0}$
110		simpr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to (r = \underset{˙}{0} \lor E (r) < E (g))$
111	14 109 110	mpjaodan	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to r = \underset{˙}{0}$
112	111	oveq2d	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to (g \cdot_{D} q) +_{D} r = (g \cdot_{D} q) +_{D} \underset{˙}{0}$
113	38	ringgrpd	$⊢ φ \to D \in Grp$
114	113	ad7antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to D \in Grp$
115	65	ad5antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to D \in Ring$
116	68	ad6antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to g \in B$
117		simp-4r	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to q \in B$
118	1 28 115 116 117	ringcld	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to g \cdot_{D} q \in B$
119	1 27 2 114 118	grpridd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to (g \cdot_{D} q) +_{D} \underset{˙}{0} = g \cdot_{D} q$
120	13 112 119	3eqtrd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to a = g \cdot_{D} q$
121	83	adantr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to q \cdot_{D} g = g \cdot_{D} q$
122	120 121	eqtr4d	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to a = q \cdot_{D} g$
123	38	adantr	$⊢ (φ \land g \in (I ∖ \{\underset{˙}{0}\})) \to D \in Ring$
124	68	snssd	$⊢ (φ \land g \in (I ∖ \{\underset{˙}{0}\})) \to \{g\} \subseteq B$
125	3 1 9	rspcl	$⊢ (D \in Ring \land \{g\} \subseteq B) \to K (\{g\}) \in LIdeal (D)$
126	123 124 125	syl2anc	$⊢ (φ \land g \in (I ∖ \{\underset{˙}{0}\})) \to K (\{g\}) \in LIdeal (D)$
127	126	ad6antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to K (\{g\}) \in LIdeal (D)$
128	1 3	rspsnid	$⊢ (D \in Ring \land g \in B) \to g \in K (\{g\})$
129	123 68 128	syl2anc	$⊢ (φ \land g \in (I ∖ \{\underset{˙}{0}\})) \to g \in K (\{g\})$
130	129	ad6antr	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to g \in K (\{g\})$
131	9 1 28 115 127 117 130	lidlmcld	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to q \cdot_{D} g \in K (\{g\})$
132	122 131	eqeltrd	$⊢ (((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land a = (g \cdot_{D} q) +_{D} r) \land (r = \underset{˙}{0} \lor E (r) < E (g))) \to a \in K (\{g\})$
133	132	anasss	$⊢ ((((((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \land q \in B) \land r \in B) \land (a = (g \cdot_{D} q) +_{D} r \land (r = \underset{˙}{0} \lor E (r) < E (g)))) \to a \in K (\{g\})$
134	6	ad3antrrr	$⊢ (((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \to D \in EDomn$
135	76 10	syl	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to I \subseteq B$
136	135	sselda	$⊢ (((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \to a \in B$
137	1 2 27 28 4 134 136 100	edomediv	$⊢ (((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \to \exists q \in B \exists r \in B (a = (g \cdot_{D} q) +_{D} r \land (r = \underset{˙}{0} \lor E (r) < E (g)))$
138	133 137	r19.29vva	$⊢ (((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \land a \in I) \to a \in K (\{g\})$
139	138	ex	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to (a \in I \to a \in K (\{g\}))$
140	139	ssrdv	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to I \subseteq K (\{g\})$
141	86	snssd	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to \{g\} \subseteq I$
142	3 9	rspssp	$⊢ (D \in Ring \land I \in LIdeal (D) \land \{g\} \subseteq I) \to K (\{g\}) \subseteq I$
143	65 76 141 142	syl3anc	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to K (\{g\}) \subseteq I$
144	140 143	eqssd	$⊢ ((φ \land g \in (I ∖ \{\underset{˙}{0}\})) \land ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M) \to I = K (\{g\})$
145		nfcv	$⊢ \underline{Ⅎ} g ({E ↾}_{(B ∖ \{\underset{˙}{0}\})})$
146	17	a1i	$⊢ φ \to < We ℕ_{0}$
147	146 21 35 55	weinfcl	$⊢ φ \to inf (E [I ∖ \{\underset{˙}{0}\}] ℕ_{0} <) \in E [I ∖ \{\underset{˙}{0}\}]$
148	5 147	eqeltrid	$⊢ φ \to M \in E [I ∖ \{\underset{˙}{0}\}]$
149	148 51	eleqtrrd	$⊢ φ \to M \in ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) [I ∖ \{\underset{˙}{0}\}]$
150	145 45 149	fvelimad	$⊢ φ \to \exists g \in ((B ∖ \{\underset{˙}{0}\}) \cap (I ∖ \{\underset{˙}{0}\})) ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M$
151		sseqin2	$⊢ I ∖ \{\underset{˙}{0}\} \subseteq B ∖ \{\underset{˙}{0}\} \leftrightarrow (B ∖ \{\underset{˙}{0}\}) \cap (I ∖ \{\underset{˙}{0}\}) = I ∖ \{\underset{˙}{0}\}$
152	23 151	sylib	$⊢ φ \to (B ∖ \{\underset{˙}{0}\}) \cap (I ∖ \{\underset{˙}{0}\}) = I ∖ \{\underset{˙}{0}\}$
153	150 152	rexeqtrdv	$⊢ φ \to \exists g \in (I ∖ \{\underset{˙}{0}\}) ({E ↾}_{(B ∖ \{\underset{˙}{0}\})}) (g) = M$
154	144 153	reximddv3	$⊢ φ \to \exists g \in (I ∖ \{\underset{˙}{0}\}) I = K (\{g\})$
155		ssrexv	$⊢ I ∖ \{\underset{˙}{0}\} \subseteq B \to (\exists g \in (I ∖ \{\underset{˙}{0}\}) I = K (\{g\}) \to \exists g \in B I = K (\{g\}))$
156	12 154 155	sylc	$⊢ φ \to \exists g \in B I = K (\{g\})$

Metamath Proof Explorer

Theorem edompidlem

Proof