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 33574

Description: Lemma for 1arithufd 33576. 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 7438	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑦 · 𝑋) = (𝑌 · 𝑋))
2	1	eqeq1d 2739	. . . 4 ⊢ (𝑦 = 𝑌 → ((𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
3		1arithufdlem3.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4	3	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑌 ∈ 𝐵)
5		simpr 484	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓))
6	2, 4, 5	rspcedvdw 3625	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓))
7		oveq2 7439	. . . . . . . 8 ⊢ (𝑧 = 𝑋 → (𝑦 · 𝑧) = (𝑦 · 𝑋))
8	7	eqeq1d 2739	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
9	8	rexbidv 3179	. . . . . 6 ⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
10		eleq1 2829	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑧 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆))
11	9, 10	imbi12d 344	. . . . 5 ⊢ (𝑧 = 𝑋 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆)))
12		oveq2 7439	. . . . . . . . . . . 12 ⊢ (𝑐 = ∅ → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g ∅))
13	12	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
14	13	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
15	14	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
16	15	ralbidv 3178	. . . . . . . 8 ⊢ (𝑐 = ∅ → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
17	16	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))))
18		oveq2 7439	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑑 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑑))
19	18	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑑 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
20	19	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
21	20	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
22	21	ralbidv 3178	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
23	22	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆))))
24		oveq2 7439	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
25	24	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
26	25	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
27	26	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
28	27	ralbidv 3178	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
29	28	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
30		oveq2 7439	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑓 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑓))
31	30	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑓 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
32	31	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑐 = 𝑓 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
33	32	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = 𝑓 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
34	33	ralbidv 3178	. . . . . . . 8 ⊢ (𝑐 = 𝑓 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
35	34	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = 𝑓 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))))
36		1arithufd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ UFD)
37	36	ufdidom 33570	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ IDomn)
38	37	idomcringd 20727	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ CRing)
39	38	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ CRing)
40		simpllr 776	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝐵)
41		simp-4r 784	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
42	41	eldifad 3963	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ (𝐵 ∖ 𝑈))
43	42	eldifad 3963	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵)
44		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (𝑀 Σ_g ∅))
45		1arithufd.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (mulGrp‘𝑅)
46		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
47	45, 46	ringidval 20180	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝑅) = (0_g‘𝑀)
48	47	gsum0 18697	. . . . . . . . . . . . . 14 ⊢ (𝑀 Σ_g ∅) = (1_r‘𝑅)
49	44, 48	eqtrdi 2793	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (1_r‘𝑅))
50	39	crngringd 20243	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ Ring)
51		1arithufd.u	. . . . . . . . . . . . . . 15 ⊢ 𝑈 = (Unit‘𝑅)
52	51, 46	1unit 20374	. . . . . . . . . . . . . 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 20381	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑦 · 𝑧) ∈ 𝑈 ↔ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)))
58	57	simplbda 499	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑦 · 𝑧) ∈ 𝑈) → 𝑧 ∈ 𝑈)
59	39, 40, 43, 54, 58	syl31anc 1375	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑈)
60	42	eldifbd 3964	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → ¬ 𝑧 ∈ 𝑈)
61	59, 60	condan 818	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
62	61	r19.29an 3158	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
63	62	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
64	63	ralrimiva 3146	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
65		oveq1 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑡) = (𝑤 · 𝑡))
66	65	eqeq1d 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → ((𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
67	66	cbvrexvw 3238	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
68		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (∥_r‘𝑅) = (∥_r‘𝑅)
69	56, 68, 55	dvdsr 20362	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑤 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤))
70		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑘 → (𝑣 · 𝑡) = (𝑘 · 𝑡))
71	70	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑘 → ((𝑣 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑)))
72		simplr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑘 ∈ 𝐵)
73		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
74		1arithufd.p	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑃 = (RPrime‘𝑅)
75	36	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑅 ∈ UFD)
76		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
77	56, 74, 75, 76	rprmcl 33546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
78	77	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝑝 ∈ 𝑃 → 𝑝 ∈ 𝐵))
79	78	ssrdv 3989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑃 ⊆ 𝐵)
80	79	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑃 ⊆ 𝐵)
81		simp-5r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝑃)
82	80, 81	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝐵)
83	82	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝐵)
84	36	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑅 ∈ UFD)
85	84	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ UFD)
86	81	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝑃)
87	74, 73, 85, 86	rprmnz 33548	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ≠ (0_g‘𝑅))
88	83, 87	eldifsnd 4787	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ (𝐵 ∖ {(0_g‘𝑅)}))
89	45, 56	mgpbas 20142	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐵 = (Base‘𝑀)
90	45	crngmgp 20238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ CRing → 𝑀 ∈ CMnd)
91	38, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑀 ∈ CMnd)
92	91	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ CMnd)
93		ovexd 7466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (0..^(♯‘𝑑)) ∈ V)
94		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (♯‘𝑑) = (♯‘𝑑))
95		sswrd 14560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ⊆ 𝐵 → Word 𝑃 ⊆ Word 𝐵)
96	79, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → Word 𝑃 ⊆ Word 𝐵)
97	96	sselda 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑑 ∈ Word 𝑃) → 𝑑 ∈ Word 𝐵)
98	97	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝐵)
99	94, 98	wrdfd 32918	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑:(0..^(♯‘𝑑))⟶𝐵)
100	38	crngringd 20243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑅 ∈ Ring)
101	100, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝑈)
102	101	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (1_r‘𝑅) ∈ 𝑈)
103		simp-6r 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝑃)
104	102, 103	wrdfsupp 32921	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 finSupp (1_r‘𝑅))
105	89, 47, 92, 93, 99, 104	gsumcl 19933	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
106	105	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
107	100	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Ring)
108		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
109	108	eldifad 3963	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ (𝐵 ∖ 𝑈))
110	109	eldifad 3963	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝐵)
111	110	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝐵)
112	56, 55, 107, 72, 111	ringcld 20257	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) ∈ 𝐵)
113	37	idomdomd 20726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ∈ Domn)
114	113	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Domn)
115	38	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ CRing)
116	56, 55, 115, 83, 106	crngcomd 20252	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = ((𝑀 Σ_g 𝑑) · 𝑝))
117		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
118	45	ringmgp 20236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
119	100, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ Mnd)
120	119	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ Mnd)
121	45, 55	mgpplusg 20141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ · = (+_g‘𝑀)
122	89, 121	gsumccatsn 18856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ Mnd ∧ 𝑑 ∈ Word 𝐵 ∧ 𝑝 ∈ 𝐵) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
123	120, 98, 82, 122	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
124	117, 123	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
125	124	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
126	56, 55, 107, 72, 83, 111	ringassd 20254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑘 · (𝑝 · 𝑡)))
127		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑝) = 𝑤)
128	127	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑤 · 𝑡))
129	56, 55, 115, 72, 83, 111	crng12d 20255	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · (𝑝 · 𝑡)) = (𝑝 · (𝑘 · 𝑡)))
130	126, 128, 129	3eqtr3d 2785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = (𝑝 · (𝑘 · 𝑡)))
131	116, 125, 130	3eqtr2d 2783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = (𝑝 · (𝑘 · 𝑡)))
132	56, 73, 55, 88, 106, 112, 114, 131	domnlcan 20721	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) = (𝑘 · 𝑡))
133	132	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑))
134	71, 72, 133	rspcedvdw 3625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
135		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑡) = (𝑣 · 𝑡))
136	135	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑)))
137	136	cbvrexvw 3238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
138	134, 137	sylibr 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑))
139		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
140		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑡 → (𝑦 · 𝑧) = (𝑦 · 𝑡))
141	140	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
142	141	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
143		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑆 ↔ 𝑡 ∈ 𝑆))
144	142, 143	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
145	144	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = 𝑡) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
146	139, 145	rspcdv 3614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
147	146	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
148	147	an72ds 32472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
149	138, 148	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
150	149	r19.29an 3158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
151	150	adantrl 716	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤)) → 𝑡 ∈ 𝑆)
152	69, 151	sylan2b 594	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑤) → 𝑡 ∈ 𝑆)
153	56, 68, 55	dvdsr 20362	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑡 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡))
154		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g 𝑓)))
155	154	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓)))
156	110	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝐵)
157		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑡”⟩))
158	157	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑡 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩)))
159		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
160	37	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ IDomn)
161	160	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑅 ∈ IDomn)
162		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑈)
163	81	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝑃)
164	163	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑃)
165	74, 51, 55, 161, 162, 164	unitmulrprm 33556	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑃)
166	159, 165	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑃)
167	166	s1cld 14641	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ⟨“𝑡”⟩ ∈ Word 𝑃)
168	89	gsumws1 18851	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑡”⟩) = 𝑡)
169	156, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑀 Σ_g ⟨“𝑡”⟩) = 𝑡)
170	169	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩))
171	158, 167, 170	rspcedvdw 3625	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓))
172	155, 156, 171	elrabd 3694	. . . . . . . . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
176		1arithufd.0	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 = (0_g‘𝑅)
177	84	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ UFD)
178	177	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑅 ∈ UFD)
179		1arithufdlem.2	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)
180	179	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ¬ 𝑅 ∈ DivRing)
181	180	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑅 ∈ DivRing)
182		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑤 → (𝑣 · 𝑘) = (𝑤 · 𝑘))
183	182	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → ((𝑣 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑)))
184		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑤 ∈ 𝐵)
185	100	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ Ring)
186		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ 𝐵)
187	56, 55, 185, 184, 186	ringcld 20257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) ∈ 𝐵)
188	105	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
189	82	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝐵)
190	74, 176, 177, 163	rprmnz 33548	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ≠ 0 )
191	189, 190	eldifsnd 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ (𝐵 ∖ { 0 }))
192	56, 55, 185, 184, 186, 189	ringassd 20254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = (𝑤 · (𝑘 · 𝑝)))
193		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑘 · 𝑝) = 𝑡)
194	193	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · (𝑘 · 𝑝)) = (𝑤 · 𝑡))
195	124	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
196	192, 194, 195	3eqtrd 2781	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = ((𝑀 Σ_g 𝑑) · 𝑝))
197	56, 176, 55, 187, 188, 191, 160, 196	idomrcan 33282	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑))
198	183, 184, 197	rspcedvdw 3625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑))
199		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑘) = (𝑣 · 𝑘))
200	199	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑)))
201	200	cbvrexvw 3238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑))
202	198, 201	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑))
203	202	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑))
204		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝐵)
205		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑘 ∈ 𝑈)
206	204, 205	eldifd 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ (𝐵 ∖ 𝑈))
207		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
208	207	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = ( 0 · 𝑝))
209		simp-6r 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = 𝑡)
210	100	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑅 ∈ Ring)
211	77	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
212	211	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑝 ∈ 𝐵)
213	56, 55, 176, 210, 212	ringlzd 20292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ( 0 · 𝑝) = 0 )
214	208, 209, 213	3eqtr3d 2785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 = 0 )
215		simp-5r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
216		eldifsni 4790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }) → 𝑡 ≠ 0 )
217	215, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ≠ 0 )
218	217	neneqd 2945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ¬ 𝑡 = 0 )
219	214, 218	pm2.65da 817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 = 0 )
220	219	neqned 2947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑘 ≠ 0 )
221	220	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ≠ 0 )
222	206, 221	eldifsnd 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
223	222	an72ds 32472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
224		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑘 → (𝑦 · 𝑧) = (𝑦 · 𝑘))
225	224	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑘 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
226	225	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
227		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (𝑧 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆))
228	226, 227	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑘 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
229	228	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑧 = 𝑘) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
230	223, 229	rspcdv 3614	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
231	230	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
232	231	an82ds 32473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
233	203, 232	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑆)
234		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑝 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g 𝑓)))
235	234	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑝 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓)))
236		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑝”⟩))
237	236	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑝 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩)))
238		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
239	238	s1cld 14641	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ⟨“𝑝”⟩ ∈ Word 𝑃)
240	89	gsumws1 18851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑝 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
241	211, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
242	241	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩))
243	237, 239, 242	rspcedvdw 3625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓))
244	235, 211, 243	elrabd 3694	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
245	244, 173	eleqtrrdi 2852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑆)
246	245	ad7antr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑆)
247	56, 176, 51, 74, 45, 178, 181, 173, 55, 233, 246	1arithufdlem2 33573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑆)
248	175, 247	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑆)
249	174, 248	pm2.61dan 813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
250	249	r19.29an 3158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
251	250	adantrl 716	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡)) → 𝑡 ∈ 𝑆)
252	153, 251	sylan2b 594	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑡) → 𝑡 ∈ 𝑆)
253		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑤 ∈ 𝐵)
254	56, 68, 55	dvdsrmul 20364	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ 𝐵 ∧ (𝑀 Σ_g 𝑑) ∈ 𝐵) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
255	82, 105, 254	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
256	255, 124	breqtrrd 5171	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)(𝑤 · 𝑡))
257	56, 74, 68, 55, 84, 81, 253, 110, 256	rprmdvds 33547	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑝(∥_r‘𝑅)𝑤 ∨ 𝑝(∥_r‘𝑅)𝑡))
258	152, 252, 257	mpjaodan 961	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
259	258	r19.29an 3158	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
260	67, 259	sylan2b 594	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
261	260	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
262	261	ralrimiva 3146	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → ∀𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
263	140	eqeq1d 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
264	263	rexbidv 3179	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
265	264, 143	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆)))
266	265	cbvralvw 3237	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆) ↔ ∀𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
267	262, 266	sylibr 234	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))
268	267	ex 412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
269	268	anasss 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃)) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
270	269	expcom 413	. . . . . . . 8 ⊢ ((𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝜑 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
271	270	a2d 29	. . . . . . 7 ⊢ ((𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃) → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
272	17, 23, 29, 35, 64, 271	wrdind 14760	. . . . . 6 ⊢ (𝑓 ∈ Word 𝑃 → (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
273	272	impcom 407	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))
274		1arithufdlem.3	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
275		1arithufdlem.4	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
276	274, 275	eldifd 3962	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈))
277		1arithufdlem.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ≠ 0 )
278	276, 277	eldifsnd 4787	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
279	278	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
280	11, 273, 279	rspcdva 3623	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆))
281	280	imp 406	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
282	6, 281	syldan 591	. 2 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
283		1arithufdlem3.1	. . . . 5 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)
284	283, 173	eleqtrdi 2851	. . . 4 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
285		eqeq1 2741	. . . . . 6 ⊢ (𝑥 = (𝑌 · 𝑋) → (𝑥 = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
286	285	rexbidv 3179	. . . . 5 ⊢ (𝑥 = (𝑌 · 𝑋) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
287	286	elrab 3692	. . . 4 ⊢ ((𝑌 · 𝑋) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)} ↔ ((𝑌 · 𝑋) ∈ 𝐵 ∧ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
288	284, 287	sylib 218	. . 3 ⊢ (𝜑 → ((𝑌 · 𝑋) ∈ 𝐵 ∧ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
289	288	simprd 495	. 2 ⊢ (𝜑 → ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓))
290	282, 289	r19.29a 3162	1 ⊢ (𝜑 → 𝑋 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3436 Vcvv 3480 ∖ cdif 3948 ⊆ wss 3951 ∅c0 4333 {csn 4626 class class class wbr 5143 ‘cfv 6561 (class class class)co 7431 0cc0 11155 ..^cfzo 13694 ♯chash 14369 Word cword 14552 ++ cconcat 14608 ⟨“cs1 14633 Basecbs 17247 ._rcmulr 17298 0_gc0g 17484 Σ_g cgsu 17485 Mndcmnd 18747 CMndccmn 19798 mulGrpcmgp 20137 1_rcur 20178 Ringcrg 20230 CRingccrg 20231 ∥_rcdsr 20354 Unitcui 20355 RPrimecrpm 20432 Domncdomn 20692 IDomncidom 20693 DivRingcdr 20729 UFDcufd 33566

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 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 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-tpos 8251 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-fz 13548 df-fzo 13695 df-seq 14043 df-hash 14370 df-word 14553 df-lsw 14601 df-concat 14609 df-s1 14634 df-substr 14679 df-pfx 14709 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-sca 17313 df-vsca 17314 df-ip 17315 df-0g 17486 df-gsum 17487 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-grp 18954 df-minusg 18955 df-sbg 18956 df-subg 19141 df-cntz 19335 df-cmn 19800 df-abl 19801 df-mgp 20138 df-rng 20150 df-ur 20179 df-ring 20232 df-cring 20233 df-oppr 20334 df-dvdsr 20357 df-unit 20358 df-invr 20388 df-rprm 20433 df-nzr 20513 df-subrg 20570 df-domn 20695 df-idom 20696 df-lmod 20860 df-lss 20930 df-lsp 20970 df-sra 21172 df-rgmod 21173 df-lidl 21218 df-rsp 21219 df-prmidl 33464 df-ufd 33567

This theorem is referenced by: 1arithufdlem4 33575

W3C validator