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 33638

Description: Lemma for 1arithufd 33640. 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 7375	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑦 · 𝑋) = (𝑌 · 𝑋))
2	1	eqeq1d 2739	. . . 4 ⊢ (𝑦 = 𝑌 → ((𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
3		1arithufdlem3.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4	3	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑌 ∈ 𝐵)
5		simpr 484	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓))
6	2, 4, 5	rspcedvdw 3581	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓))
7		oveq2 7376	. . . . . . . 8 ⊢ (𝑧 = 𝑋 → (𝑦 · 𝑧) = (𝑦 · 𝑋))
8	7	eqeq1d 2739	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
9	8	rexbidv 3162	. . . . . 6 ⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
10		eleq1 2825	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑧 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆))
11	9, 10	imbi12d 344	. . . . 5 ⊢ (𝑧 = 𝑋 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆)))
12		oveq2 7376	. . . . . . . . . . . 12 ⊢ (𝑐 = ∅ → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g ∅))
13	12	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
14	13	rexbidv 3162	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
15	14	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
16	15	ralbidv 3161	. . . . . . . 8 ⊢ (𝑐 = ∅ → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
17	16	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))))
18		oveq2 7376	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑑 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑑))
19	18	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑑 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
20	19	rexbidv 3162	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
21	20	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
22	21	ralbidv 3161	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
23	22	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆))))
24		oveq2 7376	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
25	24	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
26	25	rexbidv 3162	. . . . . . . . . 10 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
27	26	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
28	27	ralbidv 3161	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
29	28	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
30		oveq2 7376	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑓 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑓))
31	30	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑓 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
32	31	rexbidv 3162	. . . . . . . . . 10 ⊢ (𝑐 = 𝑓 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
33	32	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = 𝑓 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
34	33	ralbidv 3161	. . . . . . . 8 ⊢ (𝑐 = 𝑓 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
35	34	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = 𝑓 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))))
36		1arithufd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ UFD)
37	36	ufdidom 33634	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ IDomn)
38	37	idomcringd 20672	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ CRing)
39	38	ad4antr 733	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ CRing)
40		simpllr 776	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝐵)
41		simp-4r 784	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
42	41	eldifad 3915	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ (𝐵 ∖ 𝑈))
43	42	eldifad 3915	. . . . . . . . . . . 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 20130	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝑅) = (0_g‘𝑀)
48	47	gsum0 18621	. . . . . . . . . . . . . 14 ⊢ (𝑀 Σ_g ∅) = (1_r‘𝑅)
49	44, 48	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (1_r‘𝑅))
50	39	crngringd 20193	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ Ring)
51		1arithufd.u	. . . . . . . . . . . . . . 15 ⊢ 𝑈 = (Unit‘𝑅)
52	51, 46	1unit 20322	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝑈)
53	50, 52	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (1_r‘𝑅) ∈ 𝑈)
54	49, 53	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) ∈ 𝑈)
55		1arithufdlem3.p	. . . . . . . . . . . . . 14 ⊢ · = (._r‘𝑅)
56		1arithufd.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝑅)
57	51, 55, 56	unitmulclb 20329	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑦 · 𝑧) ∈ 𝑈 ↔ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)))
58	57	simplbda 499	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑦 · 𝑧) ∈ 𝑈) → 𝑧 ∈ 𝑈)
59	39, 40, 43, 54, 58	syl31anc 1376	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑈)
60	42	eldifbd 3916	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → ¬ 𝑧 ∈ 𝑈)
61	59, 60	condan 818	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
62	61	r19.29an 3142	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
63	62	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
64	63	ralrimiva 3130	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
65		oveq1 7375	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑡) = (𝑤 · 𝑡))
66	65	eqeq1d 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → ((𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
67	66	cbvrexvw 3217	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
68		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (∥_r‘𝑅) = (∥_r‘𝑅)
69	56, 68, 55	dvdsr 20310	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑤 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤))
70		oveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . 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 33610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
78	77	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝑝 ∈ 𝑃 → 𝑝 ∈ 𝐵))
79	78	ssrdv 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑃 ⊆ 𝐵)
80	79	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑃 ⊆ 𝐵)
81		simp-5r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝑃)
82	80, 81	sseldd 3936	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝐵)
83	82	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝐵)
84	36	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑅 ∈ UFD)
85	84	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ UFD)
86	81	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝑃)
87	74, 73, 85, 86	rprmnz 33612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ≠ (0_g‘𝑅))
88	83, 87	eldifsnd 4745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ (𝐵 ∖ {(0_g‘𝑅)}))
89	45, 56	mgpbas 20092	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐵 = (Base‘𝑀)
90	45	crngmgp 20188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ CRing → 𝑀 ∈ CMnd)
91	38, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑀 ∈ CMnd)
92	91	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ CMnd)
93		ovexd 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (0..^(♯‘𝑑)) ∈ V)
94		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (♯‘𝑑) = (♯‘𝑑))
95		sswrd 14457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ⊆ 𝐵 → Word 𝑃 ⊆ Word 𝐵)
96	79, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → Word 𝑃 ⊆ Word 𝐵)
97	96	sselda 3935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑑 ∈ Word 𝑃) → 𝑑 ∈ Word 𝐵)
98	97	ad5antr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝐵)
99	94, 98	wrdfd 14454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑:(0..^(♯‘𝑑))⟶𝐵)
100	38	crngringd 20193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑅 ∈ Ring)
101	100, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝑈)
102	101	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (1_r‘𝑅) ∈ 𝑈)
103		simp-6r 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝑃)
104	102, 103	wrdfsupp 33029	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 finSupp (1_r‘𝑅))
105	89, 47, 92, 93, 99, 104	gsumcl 19856	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
106	105	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
107	100	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Ring)
108		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
109	108	eldifad 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ (𝐵 ∖ 𝑈))
110	109	eldifad 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝐵)
111	110	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝐵)
112	56, 55, 107, 72, 111	ringcld 20207	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) ∈ 𝐵)
113	37	idomdomd 20671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ∈ Domn)
114	113	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Domn)
115	38	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ CRing)
116	56, 55, 115, 83, 106	crngcomd 20202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = ((𝑀 Σ_g 𝑑) · 𝑝))
117		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
118	45	ringmgp 20186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
119	100, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ Mnd)
120	119	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ Mnd)
121	45, 55	mgpplusg 20091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ · = (+_g‘𝑀)
122	89, 121	gsumccatsn 18780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ Mnd ∧ 𝑑 ∈ Word 𝐵 ∧ 𝑝 ∈ 𝐵) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
123	120, 98, 82, 122	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
124	117, 123	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
125	124	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
126	56, 55, 107, 72, 83, 111	ringassd 20204	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑘 · (𝑝 · 𝑡)))
127		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑝) = 𝑤)
128	127	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑤 · 𝑡))
129	56, 55, 115, 72, 83, 111	crng12d 20205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · (𝑝 · 𝑡)) = (𝑝 · (𝑘 · 𝑡)))
130	126, 128, 129	3eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = (𝑝 · (𝑘 · 𝑡)))
131	116, 125, 130	3eqtr2d 2778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = (𝑝 · (𝑘 · 𝑡)))
132	56, 73, 55, 88, 106, 112, 114, 131	domnlcan 20666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) = (𝑘 · 𝑡))
133	132	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑))
134	71, 72, 133	rspcedvdw 3581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
135		oveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑡) = (𝑣 · 𝑡))
136	135	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑)))
137	136	cbvrexvw 3217	. . . . . . . . . . . . . . . . . . . . . 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 7376	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑡 → (𝑦 · 𝑧) = (𝑦 · 𝑡))
141	140	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
142	141	rexbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
143		eleq1w 2820	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑆 ↔ 𝑡 ∈ 𝑆))
144	142, 143	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
145	144	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = 𝑡) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
146	139, 145	rspcdv 3570	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
147	146	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
148	147	an72ds 32539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
149	138, 148	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
150	149	r19.29an 3142	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
151	150	adantrl 717	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤)) → 𝑡 ∈ 𝑆)
152	69, 151	sylan2b 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑤) → 𝑡 ∈ 𝑆)
153	56, 68, 55	dvdsr 20310	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑡 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡))
154		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g 𝑓)))
155	154	rexbidv 3162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓)))
156	110	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝐵)
157		oveq2 7376	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑡”⟩))
158	157	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑡 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩)))
159		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
160	37	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝑃)
164	163	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑃)
165	74, 51, 55, 161, 162, 164	unitmulrprm 33620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑃)
166	159, 165	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑃)
167	166	s1cld 14539	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ⟨“𝑡”⟩ ∈ Word 𝑃)
168	89	gsumws1 18775	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓))
172	155, 156, 171	elrabd 3650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
173		1arithufdlem.s	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)}
174	172, 173	eleqtrrdi 2848	. . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ¬ 𝑅 ∈ DivRing)
181	180	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑅 ∈ DivRing)
182		oveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑤 → (𝑣 · 𝑘) = (𝑤 · 𝑘))
183	182	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → ((𝑣 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑)))
184		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑤 ∈ 𝐵)
185	100	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ Ring)
186		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ 𝐵)
187	56, 55, 185, 184, 186	ringcld 20207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) ∈ 𝐵)
188	105	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
189	82	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝐵)
190	74, 176, 177, 163	rprmnz 33612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ≠ 0 )
191	189, 190	eldifsnd 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ (𝐵 ∖ { 0 }))
192	56, 55, 185, 184, 186, 189	ringassd 20204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = (𝑤 · (𝑘 · 𝑝)))
193		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑘 · 𝑝) = 𝑡)
194	193	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · (𝑘 · 𝑝)) = (𝑤 · 𝑡))
195	124	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
196	192, 194, 195	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = ((𝑀 Σ_g 𝑑) · 𝑝))
197	56, 176, 55, 187, 188, 191, 160, 196	idomrcan 33372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑))
198	183, 184, 197	rspcedvdw 3581	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑))
199		oveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑘) = (𝑣 · 𝑘))
200	199	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑)))
201	200	cbvrexvw 3217	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ (𝐵 ∖ 𝑈))
207		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
208	207	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = ( 0 · 𝑝))
209		simp-6r 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = 𝑡)
210	100	ad8antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑅 ∈ Ring)
211	77	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
212	211	ad6antr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑝 ∈ 𝐵)
213	56, 55, 176, 210, 212	ringlzd 20242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ( 0 · 𝑝) = 0 )
214	208, 209, 213	3eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 = 0 )
215		simp-5r 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
216		eldifsni 4748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }) → 𝑡 ≠ 0 )
217	215, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ≠ 0 )
218	217	neneqd 2938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ¬ 𝑡 = 0 )
219	214, 218	pm2.65da 817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 = 0 )
220	219	neqned 2940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑘 ≠ 0 )
221	220	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ≠ 0 )
222	206, 221	eldifsnd 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
223	222	an72ds 32539	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
224		oveq2 7376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑘 → (𝑦 · 𝑧) = (𝑦 · 𝑘))
225	224	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑘 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
226	225	rexbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
227		eleq1w 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (𝑧 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆))
228	226, 227	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑘 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
229	228	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑧 = 𝑘) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
230	223, 229	rspcdv 3570	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
231	230	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
232	231	an82ds 32540	. . . . . . . . . . . . . . . . . . . . . . . 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 3162	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑝 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓)))
236		oveq2 7376	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑝”⟩))
237	236	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑝 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩)))
238		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
239	238	s1cld 14539	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ⟨“𝑝”⟩ ∈ Word 𝑃)
240	89	gsumws1 18775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑝 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
241	211, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
242	241	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩))
243	237, 239, 242	rspcedvdw 3581	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓))
244	235, 211, 243	elrabd 3650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
245	244, 173	eleqtrrdi 2848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑆)
246	245	ad7antr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑆)
247	56, 176, 51, 74, 45, 178, 181, 173, 55, 233, 246	1arithufdlem2 33637	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑆)
248	175, 247	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑆)
249	174, 248	pm2.61dan 813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
250	249	r19.29an 3142	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
251	250	adantrl 717	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡)) → 𝑡 ∈ 𝑆)
252	153, 251	sylan2b 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑡) → 𝑡 ∈ 𝑆)
253		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑤 ∈ 𝐵)
254	56, 68, 55	dvdsrmul 20312	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ 𝐵 ∧ (𝑀 Σ_g 𝑑) ∈ 𝐵) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
255	82, 105, 254	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
256	255, 124	breqtrrd 5128	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)(𝑤 · 𝑡))
257	56, 74, 68, 55, 84, 81, 253, 110, 256	rprmdvds 33611	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑝(∥_r‘𝑅)𝑤 ∨ 𝑝(∥_r‘𝑅)𝑡))
258	152, 252, 257	mpjaodan 961	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
259	258	r19.29an 3142	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
260	67, 259	sylan2b 595	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
261	260	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
262	261	ralrimiva 3130	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → ∀𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
263	140	eqeq1d 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
264	263	rexbidv 3162	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
265	264, 143	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆)))
266	265	cbvralvw 3216	. . . . . . . . . . . 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 14657	. . . . . 6 ⊢ (𝑓 ∈ Word 𝑃 → (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
273	272	impcom 407	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))
274		1arithufdlem.3	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
275		1arithufdlem.4	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
276	274, 275	eldifd 3914	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈))
277		1arithufdlem.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ≠ 0 )
278	276, 277	eldifsnd 4745	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
279	278	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
280	11, 273, 279	rspcdva 3579	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆))
281	280	imp 406	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
282	6, 281	syldan 592	. 2 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
283		1arithufdlem3.1	. . . . 5 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)
284	283, 173	eleqtrdi 2847	. . . 4 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
285		eqeq1 2741	. . . . . 6 ⊢ (𝑥 = (𝑌 · 𝑋) → (𝑥 = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
286	285	rexbidv 3162	. . . . 5 ⊢ (𝑥 = (𝑌 · 𝑋) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
287	286	elrab 3648	. . . 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 3146	1 ⊢ (𝜑 → 𝑋 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3401 Vcvv 3442 ∖ cdif 3900 ⊆ wss 3903 ∅c0 4287 {csn 4582 class class class wbr 5100 ‘cfv 6500 (class class class)co 7368 0cc0 11038 ..^cfzo 13582 ♯chash 14265 Word cword 14448 ++ cconcat 14505 ⟨“cs1 14531 Basecbs 17148 ._rcmulr 17190 0_gc0g 17371 Σ_g cgsu 17372 Mndcmnd 18671 CMndccmn 19721 mulGrpcmgp 20087 1_rcur 20128 Ringcrg 20180 CRingccrg 20181 ∥_rcdsr 20302 Unitcui 20303 RPrimecrpm 20380 Domncdomn 20637 IDomncidom 20638 DivRingcdr 20674 UFDcufd 33630

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-tpos 8178 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-oi 9427 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-n0 12414 df-xnn0 12487 df-z 12501 df-uz 12764 df-fz 13436 df-fzo 13583 df-seq 13937 df-hash 14266 df-word 14449 df-lsw 14498 df-concat 14506 df-s1 14532 df-substr 14577 df-pfx 14607 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-sca 17205 df-vsca 17206 df-ip 17207 df-0g 17373 df-gsum 17374 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-submnd 18721 df-grp 18878 df-minusg 18879 df-sbg 18880 df-subg 19065 df-cntz 19258 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100 df-ur 20129 df-ring 20182 df-cring 20183 df-oppr 20285 df-dvdsr 20305 df-unit 20306 df-invr 20336 df-rprm 20381 df-nzr 20458 df-subrg 20515 df-domn 20640 df-idom 20641 df-lmod 20825 df-lss 20895 df-lsp 20935 df-sra 21137 df-rgmod 21138 df-lidl 21175 df-rsp 21176 df-prmidl 33528 df-ufd 33631

This theorem is referenced by: 1arithufdlem4 33639

W3C validator