edompidlem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > edompidlem		Structured version Visualization version GIF version

Theorem edompidlem 33940

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

**Hypotheses**
Ref	Expression
edompidlem.b	⊢ 𝐵 = (Base‘𝐷)
edompidlem.o	⊢ 0 = (0_g‘𝐷)
edompidlem.k	⊢ 𝐾 = (RSpan‘𝐷)
edompidlem.e	⊢ 𝐸 = (EuclF‘𝐷)
edompidlem.m	⊢ 𝑀 = inf((𝐸 “ (𝐼 ∖ { 0 })), ℕ₀, < )
edompidlem.d	⊢ (𝜑 → 𝐷 ∈ EDomn)
edompidlem.i	⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝐷))
edompidlem.1	⊢ (𝜑 → 𝐼 ≠ { 0 })

**Assertion**
Ref	Expression
edompidlem	⊢ (𝜑 → ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔}))

Distinct variable groups: 0 ,𝑔 𝐵,𝑔 𝑔,𝐸 𝑔,𝐼 𝑔,𝑀 𝜑,𝑔 Allowed substitution hints: 𝐷(𝑔) 𝐾(𝑔)

Proof of Theorem edompidlem Dummy variables 𝑎 𝑞 𝑟 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		edompidlem.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝐷))
2		edompidlem.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐷)
3		eqid 2763	. . . . 5 ⊢ (LIdeal‘𝐷) = (LIdeal‘𝐷)
4	2, 3	lidlss 21523	. . . 4 ⊢ (𝐼 ∈ (LIdeal‘𝐷) → 𝐼 ⊆ 𝐵)
5	1, 4	syl 18	. . 3 ⊢ (𝜑 → 𝐼 ⊆ 𝐵)
6	5	ssdifssd 4086	. 2 ⊢ (𝜑 → (𝐼 ∖ { 0 }) ⊆ 𝐵)
7		simplr 781	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟))
8		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) ∧ 𝑟 = 0 ) → 𝑟 = 0 )
9		ltrel 11401	. . . . . . . . . . . . . . . . . . . 20 ⊢ Rel <
10	9	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → Rel < )
11		ltwenn0 33612	. . . . . . . . . . . . . . . . . . . 20 ⊢ < We ℕ₀
12	11	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → < We ℕ₀)
13		edompidlem.e	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐸 = (EuclF‘𝐷)
14	13	fvexi 6925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 ∈ V
15	14	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ∈ V)
16	15	imaexd 7955	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 “ (𝐼 ∖ { 0 })) ∈ V)
17	16	ad7antr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝐸 “ (𝐼 ∖ { 0 })) ∈ V)
18	5	ssdifd 4084	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐼 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 }))
19		imass2 6068	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 }) → (𝐸 “ (𝐼 ∖ { 0 })) ⊆ (𝐸 “ (𝐵 ∖ { 0 })))
20	18, 19	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 “ (𝐼 ∖ { 0 })) ⊆ (𝐸 “ (𝐵 ∖ { 0 })))
21		resima 6069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐵 ∖ { 0 })) = (𝐸 “ (𝐵 ∖ { 0 }))
22		edompidlem.d	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐷 ∈ EDomn)
23		edompidlem.o	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 = (0_g‘𝐷)
24		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (+_g‘𝐷) = (+_g‘𝐷)
25		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (._r‘𝐷) = (._r‘𝐷)
26	13	reseq1i 5978	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐸 ↾ (𝐵 ∖ { 0 })) = ((EuclF‘𝐷) ↾ (𝐵 ∖ { 0 }))
27	2, 23, 24, 25, 26	isedom 33934	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐷 ∈ EDomn ↔ (𝐷 ∈ IDomn ∧ ((𝐸 ↾ (𝐵 ∖ { 0 })):(𝐵 ∖ { 0 })⟶ℕ₀ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ { 0 })∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟) ∧ (𝑟 = 0 ∨ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑟) < ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑦))))))
28	22, 27	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐷 ∈ IDomn ∧ ((𝐸 ↾ (𝐵 ∖ { 0 })):(𝐵 ∖ { 0 })⟶ℕ₀ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐵 ∖ { 0 })∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑥 = ((𝑦(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟) ∧ (𝑟 = 0 ∨ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑟) < ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑦))))))
29	28	simprld 784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐸 ↾ (𝐵 ∖ { 0 })):(𝐵 ∖ { 0 })⟶ℕ₀)
30	29	fimassd 6756	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐵 ∖ { 0 })) ⊆ ℕ₀)
31	21, 30	eqsstrrid 3952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 “ (𝐵 ∖ { 0 })) ⊆ ℕ₀)
32	20, 31	sstrd 3923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 “ (𝐼 ∖ { 0 })) ⊆ ℕ₀)
33	32	ad7antr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝐸 “ (𝐼 ∖ { 0 })) ⊆ ℕ₀)
34	28	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐷 ∈ IDomn)
35	34	idomringd 21012	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐷 ∈ Ring)
36	3, 23	lidl0cl 21532	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝐷)) → 0 ∈ 𝐼)
37	35, 1, 36	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ∈ 𝐼)
38	37	snssd 4747	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → { 0 } ⊆ 𝐼)
39		edompidlem.1	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐼 ≠ { 0 })
40	39	necomd 3014	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → { 0 } ≠ 𝐼)
41		pssdifn0 4319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({ 0 } ⊆ 𝐼 ∧ { 0 } ≠ 𝐼) → (𝐼 ∖ { 0 }) ≠ ∅)
42	38, 40, 41	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐼 ∖ { 0 }) ≠ ∅)
43	29	ffnd 6735	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 ↾ (𝐵 ∖ { 0 })) Fn (𝐵 ∖ { 0 }))
44	43	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ { 0 })) → (𝐸 ↾ (𝐵 ∖ { 0 })) Fn (𝐵 ∖ { 0 }))
45	18	sselda 3913	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ { 0 }))
46		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ { 0 })) → 𝑥 ∈ (𝐼 ∖ { 0 }))
47	44, 45, 46	fnfvimad 7266	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ { 0 })) → ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑥) ∈ ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐼 ∖ { 0 })))
48		resima2 6070	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐼 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 }) → ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐼 ∖ { 0 })) = (𝐸 “ (𝐼 ∖ { 0 })))
49	18, 48	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐼 ∖ { 0 })) = (𝐸 “ (𝐼 ∖ { 0 })))
50	49	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ { 0 })) → ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐼 ∖ { 0 })) = (𝐸 “ (𝐼 ∖ { 0 })))
51	47, 50	eleqtrd 2866	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ { 0 })) → ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑥) ∈ (𝐸 “ (𝐼 ∖ { 0 })))
52	51	ne0d 4291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ { 0 })) → (𝐸 “ (𝐼 ∖ { 0 })) ≠ ∅)
53	42, 52	n0limd 4304	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 “ (𝐼 ∖ { 0 })) ≠ ∅)
54	53	ad7antr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝐸 “ (𝐼 ∖ { 0 })) ≠ ∅)
55	43	ad7antr 751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝐸 ↾ (𝐵 ∖ { 0 })) Fn (𝐵 ∖ { 0 }))
56		simpllr 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ 𝐵)
57		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑟 ≠ 0 )
58	56, 57	eldifsnd 4750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ (𝐵 ∖ { 0 }))
59		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟))
60	59	oveq1d 7461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝑎(-_g‘𝐷)(𝑔(._r‘𝐷)𝑞)) = (((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)(-_g‘𝐷)(𝑔(._r‘𝐷)𝑞)))
61	35	ringabld 20545	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐷 ∈ Abel)
62	61	ad7antr 751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝐷 ∈ Abel)
63	35	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → 𝐷 ∈ Ring)
64	63	ad5antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝐷 ∈ Ring)
65	18	sselda 3913	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) → 𝑔 ∈ (𝐵 ∖ { 0 }))
66	65	eldifad 4054	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) → 𝑔 ∈ 𝐵)
67	66	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑔 ∈ 𝐵)
68		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑞 ∈ 𝐵)
69	2, 25, 64, 67, 68	ringcld 20517	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝑔(._r‘𝐷)𝑞) ∈ 𝐵)
70		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (-_g‘𝐷) = (-_g‘𝐷)
71	2, 24, 70	ablpncan2 20062	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐷 ∈ Abel ∧ (𝑔(._r‘𝐷)𝑞) ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)(-_g‘𝐷)(𝑔(._r‘𝐷)𝑞)) = 𝑟)
72	62, 69, 56, 71	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)(-_g‘𝐷)(𝑔(._r‘𝐷)𝑞)) = 𝑟)
73	60, 72	eqtr2d 2799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑟 = (𝑎(-_g‘𝐷)(𝑔(._r‘𝐷)𝑞)))
74	1	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → 𝐼 ∈ (LIdeal‘𝐷))
75	74	ad5antr 747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝐼 ∈ (LIdeal‘𝐷))
76		simp-5r 798	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑎 ∈ 𝐼)
77	34	idomcringd 21011	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐷 ∈ CRing)
78	77	ad6antr 749	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) → 𝐷 ∈ CRing)
79		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) → 𝑞 ∈ 𝐵)
80	66	ad5antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) → 𝑔 ∈ 𝐵)
81	2, 25, 78, 79, 80	crngcomd 20515	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) → (𝑞(._r‘𝐷)𝑔) = (𝑔(._r‘𝐷)𝑞))
82	81	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝑞(._r‘𝐷)𝑔) = (𝑔(._r‘𝐷)𝑞))
83		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → 𝑔 ∈ (𝐼 ∖ { 0 }))
84	83	eldifad 4054	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → 𝑔 ∈ 𝐼)
85	84	ad5antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑔 ∈ 𝐼)
86	3, 2, 25, 64, 75, 68, 85	lidlmcld 21539	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝑞(._r‘𝐷)𝑔) ∈ 𝐼)
87	82, 86	eqeltrrd 2865	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝑔(._r‘𝐷)𝑞) ∈ 𝐼)
88	3, 70	lidlsubcl 21536	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐷 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝐷)) ∧ (𝑎 ∈ 𝐼 ∧ (𝑔(._r‘𝐷)𝑞) ∈ 𝐼)) → (𝑎(-_g‘𝐷)(𝑔(._r‘𝐷)𝑞)) ∈ 𝐼)
89	64, 75, 76, 87, 88	syl22anc 852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝑎(-_g‘𝐷)(𝑔(._r‘𝐷)𝑞)) ∈ 𝐼)
90	73, 89	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ 𝐼)
91	90, 57	eldifsnd 4750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ (𝐼 ∖ { 0 }))
92	55, 58, 91	fnfvimad 7266	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑟) ∈ ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐼 ∖ { 0 })))
93	58	fvresd 6931	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑟) = (𝐸‘𝑟))
94	49	ad7antr 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐼 ∖ { 0 })) = (𝐸 “ (𝐼 ∖ { 0 })))
95	92, 93, 94	3eltr3d 2878	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → (𝐸‘𝑟) ∈ (𝐸 “ (𝐼 ∖ { 0 })))
96	10, 12, 17, 33, 54, 95	weinflb 33614	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → ¬ (𝐸‘𝑟) < inf((𝐸 “ (𝐼 ∖ { 0 })), ℕ₀, < ))
97		simp-6r 800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀)
98	65	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) → 𝑔 ∈ (𝐵 ∖ { 0 }))
99	98	fvresd 6931	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) → ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = (𝐸‘𝑔))
100	99	ad4antr 745	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = (𝐸‘𝑔))
101		edompidlem.m	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑀 = inf((𝐸 “ (𝐼 ∖ { 0 })), ℕ₀, < )
102	101	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → 𝑀 = inf((𝐸 “ (𝐼 ∖ { 0 })), ℕ₀, < ))
103	97, 100, 102	3eqtr3rd 2807	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → inf((𝐸 “ (𝐼 ∖ { 0 })), ℕ₀, < ) = (𝐸‘𝑔))
104	96, 103	brneqtrd 5127	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ 𝑟 ≠ 0 ) → ¬ (𝐸‘𝑟) < (𝐸‘𝑔))
105	104	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) → (𝑟 ≠ 0 → ¬ (𝐸‘𝑟) < (𝐸‘𝑔)))
106	105	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → (𝑟 ≠ 0 → ¬ (𝐸‘𝑟) < (𝐸‘𝑔)))
107	106	necon4ad 2978	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → ((𝐸‘𝑟) < (𝐸‘𝑔) → 𝑟 = 0 ))
108	107	imp 412	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) ∧ (𝐸‘𝑟) < (𝐸‘𝑔)) → 𝑟 = 0 )
109		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔)))
110	8, 108, 109	mpjaodan 973	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝑟 = 0 )
111	110	oveq2d 7462	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟) = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷) 0 ))
112	35	ringgrpd 20502	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ Grp)
113	112	ad7antr 751	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝐷 ∈ Grp)
114	63	ad5antr 747	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝐷 ∈ Ring)
115	66	ad6antr 749	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝑔 ∈ 𝐵)
116		simp-4r 796	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝑞 ∈ 𝐵)
117	2, 25, 114, 115, 116	ringcld 20517	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → (𝑔(._r‘𝐷)𝑞) ∈ 𝐵)
118	2, 24, 23, 113, 117	grpridd 19213	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷) 0 ) = (𝑔(._r‘𝐷)𝑞))
119	7, 111, 118	3eqtrd 2802	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝑎 = (𝑔(._r‘𝐷)𝑞))
120	81	adantr 486	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → (𝑞(._r‘𝐷)𝑔) = (𝑔(._r‘𝐷)𝑞))
121	119, 120	eqtr4d 2801	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝑎 = (𝑞(._r‘𝐷)𝑔))
122	35	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) → 𝐷 ∈ Ring)
123	66	snssd 4747	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) → {𝑔} ⊆ 𝐵)
124		edompidlem.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (RSpan‘𝐷)
125	124, 2, 3	rspcl 21551	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Ring ∧ {𝑔} ⊆ 𝐵) → (𝐾‘{𝑔}) ∈ (LIdeal‘𝐷))
126	122, 123, 125	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) → (𝐾‘{𝑔}) ∈ (LIdeal‘𝐷))
127	126	ad6antr 749	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → (𝐾‘{𝑔}) ∈ (LIdeal‘𝐷))
128	2, 124	rspsnid 21560	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Ring ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐾‘{𝑔}))
129	122, 66, 128	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) → 𝑔 ∈ (𝐾‘{𝑔}))
130	129	ad6antr 749	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝑔 ∈ (𝐾‘{𝑔}))
131	3, 2, 25, 114, 127, 116, 130	lidlmcld 21539	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → (𝑞(._r‘𝐷)𝑔) ∈ (𝐾‘{𝑔}))
132	121, 131	eqeltrd 2864	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ 𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟)) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))) → 𝑎 ∈ (𝐾‘{𝑔}))
133	132	anasss 472	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) ∧ 𝑞 ∈ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔)))) → 𝑎 ∈ (𝐾‘{𝑔}))
134	22	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) → 𝐷 ∈ EDomn)
135	74, 4	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → 𝐼 ⊆ 𝐵)
136	135	sselda 3913	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐵)
137	2, 23, 24, 25, 13, 134, 136, 98	edomediv 33936	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) → ∃𝑞 ∈ 𝐵 ∃𝑟 ∈ 𝐵 (𝑎 = ((𝑔(._r‘𝐷)𝑞)(+_g‘𝐷)𝑟) ∧ (𝑟 = 0 ∨ (𝐸‘𝑟) < (𝐸‘𝑔))))
138	133, 137	r19.29vva 3226	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ (𝐾‘{𝑔}))
139	138	ex 418	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → (𝑎 ∈ 𝐼 → 𝑎 ∈ (𝐾‘{𝑔})))
140	139	ssrdv 3919	. . . 4 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → 𝐼 ⊆ (𝐾‘{𝑔}))
141	84	snssd 4747	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → {𝑔} ⊆ 𝐼)
142	124, 3	rspssp 21555	. . . . 5 ⊢ ((𝐷 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝐷) ∧ {𝑔} ⊆ 𝐼) → (𝐾‘{𝑔}) ⊆ 𝐼)
143	63, 74, 141, 142	syl3anc 1399	. . . 4 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → (𝐾‘{𝑔}) ⊆ 𝐼)
144	140, 143	eqssd 3930	. . 3 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐼 ∖ { 0 })) ∧ ((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀) → 𝐼 = (𝐾‘{𝑔}))
145		nfcv 2926	. . . . 5 ⊢ Ⅎ𝑔(𝐸 ↾ (𝐵 ∖ { 0 }))
146	11	a1i 11	. . . . . . . 8 ⊢ (𝜑 → < We ℕ₀)
147	146, 16, 32, 53	weinfcl 33613	. . . . . . 7 ⊢ (𝜑 → inf((𝐸 “ (𝐼 ∖ { 0 })), ℕ₀, < ) ∈ (𝐸 “ (𝐼 ∖ { 0 })))
148	101, 147	eqeltrid 2868	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (𝐸 “ (𝐼 ∖ { 0 })))
149	148, 49	eleqtrrd 2867	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ((𝐸 ↾ (𝐵 ∖ { 0 })) “ (𝐼 ∖ { 0 })))
150	145, 43, 149	fvelimad 6978	. . . 4 ⊢ (𝜑 → ∃𝑔 ∈ ((𝐵 ∖ { 0 }) ∩ (𝐼 ∖ { 0 }))((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀)
151		sseqin2 4123	. . . . 5 ⊢ ((𝐼 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 }) ↔ ((𝐵 ∖ { 0 }) ∩ (𝐼 ∖ { 0 })) = (𝐼 ∖ { 0 }))
152	18, 151	sylib 221	. . . 4 ⊢ (𝜑 → ((𝐵 ∖ { 0 }) ∩ (𝐼 ∖ { 0 })) = (𝐼 ∖ { 0 }))
153	150, 152	rexeqtrdv 3326	. . 3 ⊢ (𝜑 → ∃𝑔 ∈ (𝐼 ∖ { 0 })((𝐸 ↾ (𝐵 ∖ { 0 }))‘𝑔) = 𝑀)
154	144, 153	reximddv3 3183	. 2 ⊢ (𝜑 → ∃𝑔 ∈ (𝐼 ∖ { 0 })𝐼 = (𝐾‘{𝑔}))
155		ssrexv 3983	. 2 ⊢ ((𝐼 ∖ { 0 }) ⊆ 𝐵 → (∃𝑔 ∈ (𝐼 ∖ { 0 })𝐼 = (𝐾‘{𝑔}) → ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔})))
156	6, 154, 155	sylc 66	1 ⊢ (𝜑 → ∃𝑔 ∈ 𝐵 𝐼 = (𝐾‘{𝑔}))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∅c0 4281 {csn 4588 class class class wbr 5106 We wwe 5608 ↾ cres 5658 “ cima 5659 Rel wrel 5661 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7446 infcinf 9463 < clt 11373 ℕ₀cn0 12636 Basecbs 17419 +_gcplusg 17460 ._rcmulr 17461 0_gc0g 17642 Grpcgrp 19176 -_gcsg 19178 Abelcabl 20028 Ringcrg 20492 CRingccrg 20493 IDomncidom 20978 LIdealclidl 21517 RSpancrsp 21518 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-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-inf2 9672 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-er 8748 df-en 9005 df-dom 9006 df-sdom 9007 df-sup 9464 df-inf 9465 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-5 12438 df-6 12439 df-7 12440 df-8 12441 df-n0 12637 df-z 12724 df-uz 12996 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-mulr 17474 df-sca 17476 df-vsca 17477 df-ip 17478 df-0g 17644 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-grp 19179 df-minusg 19180 df-sbg 19181 df-subg 19365 df-cmn 20029 df-abl 20030 df-mgp 20394 df-rng 20408 df-ur 20441 df-ring 20494 df-cring 20495 df-subrg 20855 df-idom 20981 df-lmod 21170 df-lss 21240 df-lsp 21280 df-sra 21481 df-rgmod 21482 df-lidl 21519 df-rsp 21520 df-edom 33933

This theorem is used by: edompid 33941

W3C validator