1arithufdlem3 - Mathbox for Thierry Arnoux

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

Theorem 1arithufdlem3 33639

Description: Lemma for 1arithufd 33641. If a product (𝑌 · 𝑋) can be written as a product of primes, with 𝑋 non-unit, nonzero, so can 𝑋. (Contributed by Thierry Arnoux, 3-Jun-2025.)

**Hypotheses**
Ref	Expression
1arithufd.b	⊢ 𝐵 = (Base‘𝑅)
1arithufd.0	⊢ 0 = (0_g‘𝑅)
1arithufd.u	⊢ 𝑈 = (Unit‘𝑅)
1arithufd.p	⊢ 𝑃 = (RPrime‘𝑅)
1arithufd.m	⊢ 𝑀 = (mulGrp‘𝑅)
1arithufd.r	⊢ (𝜑 → 𝑅 ∈ UFD)
1arithufdlem.2	⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)
1arithufdlem.s	⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)}
1arithufdlem.3	⊢ (𝜑 → 𝑋 ∈ 𝐵)
1arithufdlem.4	⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
1arithufdlem.5	⊢ (𝜑 → 𝑋 ≠ 0 )
1arithufdlem3.p	⊢ · = (._r‘𝑅)
1arithufdlem3.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
1arithufdlem3.1	⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)

**Assertion**
Ref	Expression
1arithufdlem3	⊢ (𝜑 → 𝑋 ∈ 𝑆)

Distinct variable groups: 0 ,𝑓 𝑥,𝐵 𝑓,𝑀,𝑥 𝑃,𝑓,𝑥 𝑅,𝑓 𝜑,𝑓,𝑥 𝑥,𝑋 𝑥,𝑈 𝑓,𝑌,𝑥 𝑥,𝑅 𝑥,𝑆 𝑥, 0 𝑈,𝑓 𝐵,𝑓 𝑓,𝑋 · ,𝑓,𝑥 𝑆,𝑓

Proof of Theorem 1arithufdlem3 Dummy variables 𝑝 𝑐 𝑣 𝑘 𝑡 𝑤 𝑧 𝑦 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7366	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑦 · 𝑋) = (𝑌 · 𝑋))
2	1	eqeq1d 2743	. . . 4 ⊢ (𝑦 = 𝑌 → ((𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
3		1arithufdlem3.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4	3	ad2antrr 733	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑌 ∈ 𝐵)
5		simpr 486	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓))
6	2, 4, 5	rspcedvdw 3564	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓))
7		oveq2 7367	. . . . . . . 8 ⊢ (𝑧 = 𝑋 → (𝑦 · 𝑧) = (𝑦 · 𝑋))
8	7	eqeq1d 2743	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
9	8	rexbidv 3165	. . . . . 6 ⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
10		eleq1 2829	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑧 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆))
11	9, 10	imbi12d 346	. . . . 5 ⊢ (𝑧 = 𝑋 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆)))
12		oveq2 7367	. . . . . . . . . . . 12 ⊢ (𝑐 = ∅ → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g ∅))
13	12	eqeq2d 2752	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
14	13	rexbidv 3165	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
15	14	imbi1d 343	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
16	15	ralbidv 3164	. . . . . . . 8 ⊢ (𝑐 = ∅ → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
17	16	imbi2d 342	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))))
18		oveq2 7367	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑑 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑑))
19	18	eqeq2d 2752	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑑 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
20	19	rexbidv 3165	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
21	20	imbi1d 343	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
22	21	ralbidv 3164	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
23	22	imbi2d 342	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆))))
24		oveq2 7367	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
25	24	eqeq2d 2752	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
26	25	rexbidv 3165	. . . . . . . . . 10 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
27	26	imbi1d 343	. . . . . . . . 9 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
28	27	ralbidv 3164	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
29	28	imbi2d 342	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
30		oveq2 7367	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑓 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑓))
31	30	eqeq2d 2752	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑓 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
32	31	rexbidv 3165	. . . . . . . . . 10 ⊢ (𝑐 = 𝑓 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
33	32	imbi1d 343	. . . . . . . . 9 ⊢ (𝑐 = 𝑓 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
34	33	ralbidv 3164	. . . . . . . 8 ⊢ (𝑐 = 𝑓 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
35	34	imbi2d 342	. . . . . . 7 ⊢ (𝑐 = 𝑓 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))))
36		1arithufd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ UFD)
37	36	ufdidom 33635	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ IDomn)
38	37	idomcringd 20702	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ CRing)
39	38	ad4antr 739	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ CRing)
40		simpllr 782	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝐵)
41		simp-4r 790	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
42	41	eldifad 3896	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ (𝐵 ∖ 𝑈))
43	42	eldifad 3896	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵)
44		simplr 775	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (𝑀 Σ_g ∅))
45		1arithufd.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (mulGrp‘𝑅)
46		eqid 2741	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
47	45, 46	ringidval 20158	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝑅) = (0_g‘𝑀)
48	47	gsum0 18647	. . . . . . . . . . . . . 14 ⊢ (𝑀 Σ_g ∅) = (1_r‘𝑅)
49	44, 48	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (1_r‘𝑅))
50	39	crngringd 20221	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ Ring)
51		1arithufd.u	. . . . . . . . . . . . . . 15 ⊢ 𝑈 = (Unit‘𝑅)
52	51, 46	1unit 20348	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝑈)
53	50, 52	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (1_r‘𝑅) ∈ 𝑈)
54	49, 53	eqeltrd 2841	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) ∈ 𝑈)
55		1arithufdlem3.p	. . . . . . . . . . . . . 14 ⊢ · = (._r‘𝑅)
56		1arithufd.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝑅)
57	51, 55, 56	unitmulclb 20355	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑦 · 𝑧) ∈ 𝑈 ↔ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)))
58	57	simplbda 501	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑦 · 𝑧) ∈ 𝑈) → 𝑧 ∈ 𝑈)
59	39, 40, 43, 54, 58	syl31anc 1382	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑈)
60	42	eldifbd 3897	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → ¬ 𝑧 ∈ 𝑈)
61	59, 60	condan 824	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
62	61	r19.29an 3145	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
63	62	ex 414	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
64	63	ralrimiva 3133	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
65		oveq1 7366	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑡) = (𝑤 · 𝑡))
66	65	eqeq1d 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → ((𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
67	66	cbvrexvw 3220	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
68		eqid 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (∥_r‘𝑅) = (∥_r‘𝑅)
69	56, 68, 55	dvdsr 20336	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑤 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤))
70		oveq1 7366	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑘 → (𝑣 · 𝑡) = (𝑘 · 𝑡))
71	70	eqeq1d 2743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑘 → ((𝑣 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑)))
72		simplr 775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑘 ∈ 𝐵)
73		eqid 2741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
74		1arithufd.p	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑃 = (RPrime‘𝑅)
75	36	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑅 ∈ UFD)
76		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
77	56, 74, 75, 76	rprmcl 33611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
78	77	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝑝 ∈ 𝑃 → 𝑝 ∈ 𝐵))
79	78	ssrdv 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑃 ⊆ 𝐵)
80	79	ad6antr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑃 ⊆ 𝐵)
81		simp-5r 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝑃)
82	80, 81	sseldd 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝐵)
83	82	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝐵)
84	36	ad6antr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑅 ∈ UFD)
85	84	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ UFD)
86	81	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝑃)
87	74, 73, 85, 86	rprmnz 33613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ≠ (0_g‘𝑅))
88	83, 87	eldifsnd 4722	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ (𝐵 ∖ {(0_g‘𝑅)}))
89	45, 56	mgpbas 20120	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐵 = (Base‘𝑀)
90	45	crngmgp 20216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ CRing → 𝑀 ∈ CMnd)
91	38, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑀 ∈ CMnd)
92	91	ad6antr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ CMnd)
93		ovexd 7394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (0..^(♯‘𝑑)) ∈ V)
94		eqidd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (♯‘𝑑) = (♯‘𝑑))
95		sswrd 14479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ⊆ 𝐵 → Word 𝑃 ⊆ Word 𝐵)
96	79, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → Word 𝑃 ⊆ Word 𝐵)
97	96	sselda 3916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑑 ∈ Word 𝑃) → 𝑑 ∈ Word 𝐵)
98	97	ad5antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝐵)
99	94, 98	wrdfd 14476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑:(0..^(♯‘𝑑))⟶𝐵)
100	38	crngringd 20221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑅 ∈ Ring)
101	100, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝑈)
102	101	ad6antr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (1_r‘𝑅) ∈ 𝑈)
103		simp-6r 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝑃)
104	102, 103	wrdfsupp 33018	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 finSupp (1_r‘𝑅))
105	89, 47, 92, 93, 99, 104	gsumcl 19884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
106	105	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
107	100	ad8antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Ring)
108		simpllr 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
109	108	eldifad 3896	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ (𝐵 ∖ 𝑈))
110	109	eldifad 3896	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝐵)
111	110	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝐵)
112	56, 55, 107, 72, 111	ringcld 20235	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) ∈ 𝐵)
113	37	idomdomd 20701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ∈ Domn)
114	113	ad8antr 747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Domn)
115	38	ad8antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ CRing)
116	56, 55, 115, 83, 106	crngcomd 20230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = ((𝑀 Σ_g 𝑑) · 𝑝))
117		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
118	45	ringmgp 20214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
119	100, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ Mnd)
120	119	ad6antr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ Mnd)
121	45, 55	mgpplusg 20119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ · = (+_g‘𝑀)
122	89, 121	gsumccatsn 18806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ Mnd ∧ 𝑑 ∈ Word 𝐵 ∧ 𝑝 ∈ 𝐵) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
123	120, 98, 82, 122	syl3anc 1380	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
124	117, 123	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
125	124	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
126	56, 55, 107, 72, 83, 111	ringassd 20232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑘 · (𝑝 · 𝑡)))
127		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑝) = 𝑤)
128	127	oveq1d 7374	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑤 · 𝑡))
129	56, 55, 115, 72, 83, 111	crng12d 20233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · (𝑝 · 𝑡)) = (𝑝 · (𝑘 · 𝑡)))
130	126, 128, 129	3eqtr3d 2784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = (𝑝 · (𝑘 · 𝑡)))
131	116, 125, 130	3eqtr2d 2782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = (𝑝 · (𝑘 · 𝑡)))
132	56, 73, 55, 88, 106, 112, 114, 131	domnlcan 20696	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) = (𝑘 · 𝑡))
133	132	eqcomd 2747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑))
134	71, 72, 133	rspcedvdw 3564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
135		oveq1 7366	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑡) = (𝑣 · 𝑡))
136	135	eqeq1d 2743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑)))
137	136	cbvrexvw 3220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
138	134, 137	sylibr 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑))
139		simp-4r 790	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
140		oveq2 7367	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑡 → (𝑦 · 𝑧) = (𝑦 · 𝑡))
141	140	eqeq1d 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
142	141	rexbidv 3165	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
143		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑆 ↔ 𝑡 ∈ 𝑆))
144	142, 143	imbi12d 346	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
145	144	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = 𝑡) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
146	139, 145	rspcdv 3553	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
147	146	imp 408	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
148	147	an72ds 32543	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
149	138, 148	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
150	149	r19.29an 3145	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
151	150	adantrl 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤)) → 𝑡 ∈ 𝑆)
152	69, 151	sylan2b 601	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑤) → 𝑡 ∈ 𝑆)
153	56, 68, 55	dvdsr 20336	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑡 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡))
154		eqeq1 2745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g 𝑓)))
155	154	rexbidv 3165	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓)))
156	110	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝐵)
157		oveq2 7367	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑡”⟩))
158	157	eqeq2d 2752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑡 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩)))
159		simplr 775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
160	37	ad8antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ IDomn)
161	160	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑅 ∈ IDomn)
162		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑈)
163	81	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝑃)
164	163	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑃)
165	74, 51, 55, 161, 162, 164	unitmulrprm 33621	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑃)
166	159, 165	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑃)
167	166	s1cld 14561	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ⟨“𝑡”⟩ ∈ Word 𝑃)
168	89	gsumws1 18801	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑡”⟩) = 𝑡)
169	156, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑀 Σ_g ⟨“𝑡”⟩) = 𝑡)
170	169	eqcomd 2747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩))
171	158, 167, 170	rspcedvdw 3564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓))
172	155, 156, 171	elrabd 3632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
173		1arithufdlem.s	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)}
174	172, 173	eleqtrrdi 2852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑆)
175		simplr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
176		1arithufd.0	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 = (0_g‘𝑅)
177	84	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ UFD)
178	177	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑅 ∈ UFD)
179		1arithufdlem.2	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)
180	179	ad8antr 747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ¬ 𝑅 ∈ DivRing)
181	180	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑅 ∈ DivRing)
182		oveq1 7366	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑤 → (𝑣 · 𝑘) = (𝑤 · 𝑘))
183	182	eqeq1d 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → ((𝑣 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑)))
184		simp-4r 790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑤 ∈ 𝐵)
185	100	ad8antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ Ring)
186		simplr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ 𝐵)
187	56, 55, 185, 184, 186	ringcld 20235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) ∈ 𝐵)
188	105	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
189	82	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝐵)
190	74, 176, 177, 163	rprmnz 33613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ≠ 0 )
191	189, 190	eldifsnd 4722	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ (𝐵 ∖ { 0 }))
192	56, 55, 185, 184, 186, 189	ringassd 20232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = (𝑤 · (𝑘 · 𝑝)))
193		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑘 · 𝑝) = 𝑡)
194	193	oveq2d 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · (𝑘 · 𝑝)) = (𝑤 · 𝑡))
195	124	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
196	192, 194, 195	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = ((𝑀 Σ_g 𝑑) · 𝑝))
197	56, 176, 55, 187, 188, 191, 160, 196	idomrcan 33362	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑))
198	183, 184, 197	rspcedvdw 3564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑))
199		oveq1 7366	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑘) = (𝑣 · 𝑘))
200	199	eqeq1d 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑)))
201	200	cbvrexvw 3220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑))
202	198, 201	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑))
203	202	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑))
204		simplr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝐵)
205		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑘 ∈ 𝑈)
206	204, 205	eldifd 3895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ (𝐵 ∖ 𝑈))
207		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
208	207	oveq1d 7374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = ( 0 · 𝑝))
209		simp-6r 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = 𝑡)
210	100	ad8antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑅 ∈ Ring)
211	77	adantlr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
212	211	ad6antr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑝 ∈ 𝐵)
213	56, 55, 176, 210, 212	ringlzd 20270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ( 0 · 𝑝) = 0 )
214	208, 209, 213	3eqtr3d 2784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 = 0 )
215		simp-5r 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
216		eldifsni 4725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }) → 𝑡 ≠ 0 )
217	215, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ≠ 0 )
218	217	neneqd 2941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ¬ 𝑡 = 0 )
219	214, 218	pm2.65da 823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 = 0 )
220	219	neqned 2943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑘 ≠ 0 )
221	220	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ≠ 0 )
222	206, 221	eldifsnd 4722	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
223	222	an72ds 32543	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
224		oveq2 7367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑘 → (𝑦 · 𝑧) = (𝑦 · 𝑘))
225	224	eqeq1d 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑘 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
226	225	rexbidv 3165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
227		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (𝑧 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆))
228	226, 227	imbi12d 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑘 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
229	228	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑧 = 𝑘) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
230	223, 229	rspcdv 3553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
231	230	imp 408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
232	231	an82ds 32544	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
233	203, 232	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑆)
234		eqeq1 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑝 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g 𝑓)))
235	234	rexbidv 3165	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑝 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓)))
236		oveq2 7367	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑝”⟩))
237	236	eqeq2d 2752	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑝 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩)))
238		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
239	238	s1cld 14561	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ⟨“𝑝”⟩ ∈ Word 𝑃)
240	89	gsumws1 18801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑝 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
241	211, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
242	241	eqcomd 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩))
243	237, 239, 242	rspcedvdw 3564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓))
244	235, 211, 243	elrabd 3632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
245	244, 173	eleqtrrdi 2852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑆)
246	245	ad7antr 745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑆)
247	56, 176, 51, 74, 45, 178, 181, 173, 55, 233, 246	1arithufdlem2 33638	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑆)
248	175, 247	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑆)
249	174, 248	pm2.61dan 819	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
250	249	r19.29an 3145	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
251	250	adantrl 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡)) → 𝑡 ∈ 𝑆)
252	153, 251	sylan2b 601	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑡) → 𝑡 ∈ 𝑆)
253		simplr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑤 ∈ 𝐵)
254	56, 68, 55	dvdsrmul 20338	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ 𝐵 ∧ (𝑀 Σ_g 𝑑) ∈ 𝐵) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
255	82, 105, 254	syl2anc 591	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
256	255, 124	breqtrrd 5102	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)(𝑤 · 𝑡))
257	56, 74, 68, 55, 84, 81, 253, 110, 256	rprmdvds 33612	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑝(∥_r‘𝑅)𝑤 ∨ 𝑝(∥_r‘𝑅)𝑡))
258	152, 252, 257	mpjaodan 967	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
259	258	r19.29an 3145	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
260	67, 259	sylan2b 601	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
261	260	ex 414	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
262	261	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → ∀𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
263	140	eqeq1d 2743	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
264	263	rexbidv 3165	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
265	264, 143	imbi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆)))
266	265	cbvralvw 3219	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆) ↔ ∀𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
267	262, 266	sylibr 236	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))
268	267	ex 414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
269	268	anasss 468	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃)) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
270	269	expcom 415	. . . . . . . 8 ⊢ ((𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝜑 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
271	270	a2d 29	. . . . . . 7 ⊢ ((𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃) → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
272	17, 23, 29, 35, 64, 271	wrdind 14679	. . . . . 6 ⊢ (𝑓 ∈ Word 𝑃 → (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
273	272	impcom 409	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))
274		1arithufdlem.3	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
275		1arithufdlem.4	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
276	274, 275	eldifd 3895	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈))
277		1arithufdlem.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ≠ 0 )
278	276, 277	eldifsnd 4722	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
279	278	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
280	11, 273, 279	rspcdva 3562	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆))
281	280	imp 408	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
282	6, 281	syldan 598	. 2 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
283		1arithufdlem3.1	. . . . 5 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)
284	283, 173	eleqtrdi 2851	. . . 4 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
285		eqeq1 2745	. . . . . 6 ⊢ (𝑥 = (𝑌 · 𝑋) → (𝑥 = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
286	285	rexbidv 3165	. . . . 5 ⊢ (𝑥 = (𝑌 · 𝑋) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
287	286	elrab 3630	. . . 4 ⊢ ((𝑌 · 𝑋) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)} ↔ ((𝑌 · 𝑋) ∈ 𝐵 ∧ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
288	284, 287	sylib 220	. . 3 ⊢ (𝜑 → ((𝑌 · 𝑋) ∈ 𝐵 ∧ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
289	288	simprd 497	. 2 ⊢ (𝜑 → ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓))
290	282, 289	r19.29a 3149	1 ⊢ (𝜑 → 𝑋 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 397 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∀wral 3055 ∃wrex 3065 {crab 3393 Vcvv 3433 ∖ cdif 3881 ⊆ wss 3884 ∅c0 4263 {csn 4557 class class class wbr 5074 ‘cfv 6488 (class class class)co 7359 0cc0 11034 ..^cfzo 13603 ♯chash 14287 Word cword 14470 ++ cconcat 14527 ⟨“cs1 14553 Basecbs 17174 ._rcmulr 17216 0_gc0g 17397 Σ_g cgsu 17398 Mndcmnd 18697 CMndccmn 19749 mulGrpcmgp 20115 1_rcur 20156 Ringcrg 20208 CRingccrg 20209 ∥_rcdsr 20328 Unitcui 20329 RPrimecrpm 20406 Domncdomn 20667 IDomncidom 20668 DivRingcdr 20704 UFDcufd 33631

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7681 ax-cnex 11090 ax-resscn 11091 ax-1cn 11092 ax-icn 11093 ax-addcl 11094 ax-addrcl 11095 ax-mulcl 11096 ax-mulrcl 11097 ax-mulcom 11098 ax-addass 11099 ax-mulass 11100 ax-distr 11101 ax-i2m1 11102 ax-1ne0 11103 ax-1rid 11104 ax-rnegex 11105 ax-rrecex 11106 ax-cnre 11107 ax-pre-lttri 11108 ax-pre-lttrn 11109 ax-pre-ltadd 11110 ax-pre-mulgt0 11111

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3725 df-csb 3833 df-dif 3887 df-un 3889 df-in 3891 df-ss 3901 df-pss 3904 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4841 df-int 4880 df-iun 4925 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-se 5574 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7316 df-ov 7362 df-oprab 7363 df-mpo 7364 df-om 7810 df-1st 7933 df-2nd 7934 df-supp 8103 df-tpos 8168 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8343 df-1o 8399 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-oi 9419 df-card 9858 df-pnf 11177 df-mnf 11178 df-xr 11179 df-ltxr 11180 df-le 11181 df-sub 11375 df-neg 11376 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-7 12244 df-8 12245 df-n0 12433 df-xnn0 12506 df-z 12520 df-uz 12784 df-fz 13457 df-fzo 13604 df-seq 13959 df-hash 14288 df-word 14471 df-lsw 14520 df-concat 14528 df-s1 14554 df-substr 14599 df-pfx 14629 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-sca 17231 df-vsca 17232 df-ip 17233 df-0g 17399 df-gsum 17400 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18747 df-grp 18907 df-minusg 18908 df-sbg 18909 df-subg 19094 df-cntz 19286 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-ring 20210 df-cring 20211 df-oppr 20311 df-dvdsr 20331 df-unit 20332 df-invr 20362 df-rprm 20407 df-nzr 20488 df-subrg 20545 df-domn 20670 df-idom 20671 df-lmod 20855 df-lss 20925 df-lsp 20965 df-sra 21166 df-rgmod 21167 df-lidl 21204 df-rsp 21205 df-prmidl 33521 df-ufd 33632

This theorem is referenced by: 1arithufdlem4 33640

W3C validator