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 33753

Description: Lemma for 1arithufd 33755. 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 7407	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑦 · 𝑋) = (𝑌 · 𝑋))
2	1	eqeq1d 2767	. . . 4 ⊢ (𝑦 = 𝑌 → ((𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
3		1arithufdlem3.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4	3	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑌 ∈ 𝐵)
5		simpr 489	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓))
6	2, 4, 5	rspcedvdw 3587	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓))
7		oveq2 7408	. . . . . . . 8 ⊢ (𝑧 = 𝑋 → (𝑦 · 𝑧) = (𝑦 · 𝑋))
8	7	eqeq1d 2767	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
9	8	rexbidv 3189	. . . . . 6 ⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
10		eleq1 2853	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑧 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆))
11	9, 10	imbi12d 347	. . . . 5 ⊢ (𝑧 = 𝑋 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆)))
12		oveq2 7408	. . . . . . . . . . . 12 ⊢ (𝑐 = ∅ → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g ∅))
13	12	eqeq2d 2776	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
14	13	rexbidv 3189	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
15	14	imbi1d 344	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
16	15	ralbidv 3188	. . . . . . . 8 ⊢ (𝑐 = ∅ → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
17	16	imbi2d 343	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))))
18		oveq2 7408	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑑 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑑))
19	18	eqeq2d 2776	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑑 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
20	19	rexbidv 3189	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
21	20	imbi1d 344	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
22	21	ralbidv 3188	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
23	22	imbi2d 343	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆))))
24		oveq2 7408	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
25	24	eqeq2d 2776	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
26	25	rexbidv 3189	. . . . . . . . . 10 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
27	26	imbi1d 344	. . . . . . . . 9 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
28	27	ralbidv 3188	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
29	28	imbi2d 343	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
30		oveq2 7408	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑓 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑓))
31	30	eqeq2d 2776	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑓 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
32	31	rexbidv 3189	. . . . . . . . . 10 ⊢ (𝑐 = 𝑓 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
33	32	imbi1d 344	. . . . . . . . 9 ⊢ (𝑐 = 𝑓 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
34	33	ralbidv 3188	. . . . . . . 8 ⊢ (𝑐 = 𝑓 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
35	34	imbi2d 343	. . . . . . 7 ⊢ (𝑐 = 𝑓 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))))
36		1arithufd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ UFD)
37	36	ufdidom 33749	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ IDomn)
38	37	idomcringd 20802	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ CRing)
39	38	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ CRing)
40		simpllr 787	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝐵)
41		simp-4r 795	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
42	41	eldifad 3919	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ (𝐵 ∖ 𝑈))
43	42	eldifad 3919	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵)
44		simplr 780	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (𝑀 Σ_g ∅))
45		1arithufd.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (mulGrp‘𝑅)
46		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
47	45, 46	ringidval 20256	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝑅) = (0_g‘𝑀)
48	47	gsum0 18732	. . . . . . . . . . . . . 14 ⊢ (𝑀 Σ_g ∅) = (1_r‘𝑅)
49	44, 48	eqtrdi 2816	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (1_r‘𝑅))
50	39	crngringd 20319	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ Ring)
51		1arithufd.u	. . . . . . . . . . . . . . 15 ⊢ 𝑈 = (Unit‘𝑅)
52	51, 46	1unit 20447	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝑈)
53	50, 52	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (1_r‘𝑅) ∈ 𝑈)
54	49, 53	eqeltrd 2865	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) ∈ 𝑈)
55		1arithufdlem3.p	. . . . . . . . . . . . . 14 ⊢ · = (._r‘𝑅)
56		1arithufd.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝑅)
57	51, 55, 56	unitmulclb 20454	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑦 · 𝑧) ∈ 𝑈 ↔ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)))
58	57	simplbda 504	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑦 · 𝑧) ∈ 𝑈) → 𝑧 ∈ 𝑈)
59	39, 40, 43, 54, 58	syl31anc 1396	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑈)
60	42	eldifbd 3920	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → ¬ 𝑧 ∈ 𝑈)
61	59, 60	condan 829	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
62	61	r19.29an 3169	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
63	62	ex 417	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
64	63	ralrimiva 3157	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
65		oveq1 7407	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑡) = (𝑤 · 𝑡))
66	65	eqeq1d 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → ((𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
67	66	cbvrexvw 3244	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
68		eqid 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (∥_r‘𝑅) = (∥_r‘𝑅)
69	56, 68, 55	dvdsr 20435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑤 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤))
70		oveq1 7407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑘 → (𝑣 · 𝑡) = (𝑘 · 𝑡))
71	70	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑘 → ((𝑣 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑)))
72		simplr 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑘 ∈ 𝐵)
73		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
74		1arithufd.p	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑃 = (RPrime‘𝑅)
75	36	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑅 ∈ UFD)
76		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
77	56, 74, 75, 76	rprmcl 33725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
78	77	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝑝 ∈ 𝑃 → 𝑝 ∈ 𝐵))
79	78	ssrdv 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑃 ⊆ 𝐵)
80	79	ad6antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑃 ⊆ 𝐵)
81		simp-5r 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝑃)
82	80, 81	sseldd 3940	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝐵)
83	82	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝐵)
84	36	ad6antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑅 ∈ UFD)
85	84	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ UFD)
86	81	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝑃)
87	74, 73, 85, 86	rprmnz 33727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ≠ (0_g‘𝑅))
88	83, 87	eldifsnd 4750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ (𝐵 ∖ {(0_g‘𝑅)}))
89	45, 56	mgpbas 20212	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐵 = (Base‘𝑀)
90	45	crngmgp 20314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ CRing → 𝑀 ∈ CMnd)
91	38, 90	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑀 ∈ CMnd)
92	91	ad6antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ CMnd)
93		ovexd 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (0..^(♯‘𝑑)) ∈ V)
94		eqidd 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (♯‘𝑑) = (♯‘𝑑))
95		sswrd 14549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ⊆ 𝐵 → Word 𝑃 ⊆ Word 𝐵)
96	79, 95	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → Word 𝑃 ⊆ Word 𝐵)
97	96	sselda 3939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑑 ∈ Word 𝑃) → 𝑑 ∈ Word 𝐵)
98	97	ad5antr 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝐵)
99	94, 98	wrdfd 14546	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑:(0..^(♯‘𝑑))⟶𝐵)
100	38	crngringd 20319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑅 ∈ Ring)
101	100, 52	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝑈)
102	101	ad6antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (1_r‘𝑅) ∈ 𝑈)
103		simp-6r 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝑃)
104	102, 103	wrdfsupp 33170	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 finSupp (1_r‘𝑅))
105	89, 47, 92, 93, 99, 104	gsumcl 19976	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
106	105	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
107	100	ad8antr 752	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Ring)
108		simpllr 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
109	108	eldifad 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ (𝐵 ∖ 𝑈))
110	109	eldifad 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝐵)
111	110	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝐵)
112	56, 55, 107, 72, 111	ringcld 20333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) ∈ 𝐵)
113	37	idomdomd 20801	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ∈ Domn)
114	113	ad8antr 752	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Domn)
115	38	ad8antr 752	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ CRing)
116	56, 55, 115, 83, 106	crngcomd 20328	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = ((𝑀 Σ_g 𝑑) · 𝑝))
117		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
118	45	ringmgp 20312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
119	100, 118	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ Mnd)
120	119	ad6antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ Mnd)
121	45, 55	mgpplusg 20211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ · = (+_g‘𝑀)
122	89, 121	gsumccatsn 18892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ Mnd ∧ 𝑑 ∈ Word 𝐵 ∧ 𝑝 ∈ 𝐵) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
123	120, 98, 82, 122	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
124	117, 123	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
125	124	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
126	56, 55, 107, 72, 83, 111	ringassd 20330	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑘 · (𝑝 · 𝑡)))
127		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑝) = 𝑤)
128	127	oveq1d 7415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑤 · 𝑡))
129	56, 55, 115, 72, 83, 111	crng12d 20331	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · (𝑝 · 𝑡)) = (𝑝 · (𝑘 · 𝑡)))
130	126, 128, 129	3eqtr3d 2808	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = (𝑝 · (𝑘 · 𝑡)))
131	116, 125, 130	3eqtr2d 2806	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = (𝑝 · (𝑘 · 𝑡)))
132	56, 73, 55, 88, 106, 112, 114, 131	domnlcan 20796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) = (𝑘 · 𝑡))
133	132	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑))
134	71, 72, 133	rspcedvdw 3587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
135		oveq1 7407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑡) = (𝑣 · 𝑡))
136	135	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑)))
137	136	cbvrexvw 3244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
138	134, 137	sylibr 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑))
139		simp-4r 795	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
140		oveq2 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑡 → (𝑦 · 𝑧) = (𝑦 · 𝑡))
141	140	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
142	141	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
143		eleq1w 2848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑆 ↔ 𝑡 ∈ 𝑆))
144	142, 143	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
145	144	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = 𝑡) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
146	139, 145	rspcdv 3576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
147	146	imp 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
148	147	an72ds 32713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
149	138, 148	mpd 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
150	149	r19.29an 3169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
151	150	adantrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤)) → 𝑡 ∈ 𝑆)
152	69, 151	sylan2b 605	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑤) → 𝑡 ∈ 𝑆)
153	56, 68, 55	dvdsr 20435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑡 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡))
154		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g 𝑓)))
155	154	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓)))
156	110	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝐵)
157		oveq2 7408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑡”⟩))
158	157	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑡 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩)))
159		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
160	37	ad8antr 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ IDomn)
161	160	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑅 ∈ IDomn)
162		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑈)
163	81	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝑃)
164	163	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑃)
165	74, 51, 55, 161, 162, 164	unitmulrprm 33735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑃)
166	159, 165	eqeltrrd 2866	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑃)
167	166	s1cld 14631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ⟨“𝑡”⟩ ∈ Word 𝑃)
168	89	gsumws1 18887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑡”⟩) = 𝑡)
169	156, 168	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑀 Σ_g ⟨“𝑡”⟩) = 𝑡)
170	169	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩))
171	158, 167, 170	rspcedvdw 3587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓))
172	155, 156, 171	elrabd 3655	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
173		1arithufdlem.s	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)}
174	172, 173	eleqtrrdi 2876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑆)
175		simplr 780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
176		1arithufd.0	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 = (0_g‘𝑅)
177	84	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ UFD)
178	177	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑅 ∈ UFD)
179		1arithufdlem.2	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)
180	179	ad8antr 752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ¬ 𝑅 ∈ DivRing)
181	180	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑅 ∈ DivRing)
182		oveq1 7407	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑤 → (𝑣 · 𝑘) = (𝑤 · 𝑘))
183	182	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → ((𝑣 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑)))
184		simp-4r 795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑤 ∈ 𝐵)
185	100	ad8antr 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ Ring)
186		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ 𝐵)
187	56, 55, 185, 184, 186	ringcld 20333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) ∈ 𝐵)
188	105	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
189	82	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝐵)
190	74, 176, 177, 163	rprmnz 33727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ≠ 0 )
191	189, 190	eldifsnd 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ (𝐵 ∖ { 0 }))
192	56, 55, 185, 184, 186, 189	ringassd 20330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = (𝑤 · (𝑘 · 𝑝)))
193		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑘 · 𝑝) = 𝑡)
194	193	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · (𝑘 · 𝑝)) = (𝑤 · 𝑡))
195	124	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
196	192, 194, 195	3eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = ((𝑀 Σ_g 𝑑) · 𝑝))
197	56, 176, 55, 187, 188, 191, 160, 196	idomrcan 33515	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑))
198	183, 184, 197	rspcedvdw 3587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑))
199		oveq1 7407	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑘) = (𝑣 · 𝑘))
200	199	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑)))
201	200	cbvrexvw 3244	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑))
202	198, 201	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑))
203	202	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑))
204		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝐵)
205		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑘 ∈ 𝑈)
206	204, 205	eldifd 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ (𝐵 ∖ 𝑈))
207		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
208	207	oveq1d 7415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = ( 0 · 𝑝))
209		simp-6r 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = 𝑡)
210	100	ad8antr 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑅 ∈ Ring)
211	77	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
212	211	ad6antr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑝 ∈ 𝐵)
213	56, 55, 176, 210, 212	ringlzd 20369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ( 0 · 𝑝) = 0 )
214	208, 209, 213	3eqtr3d 2808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 = 0 )
215		simp-5r 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
216		eldifsni 4753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }) → 𝑡 ≠ 0 )
217	215, 216	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ≠ 0 )
218	217	neneqd 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ¬ 𝑡 = 0 )
219	214, 218	pm2.65da 828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 = 0 )
220	219	neqned 2967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑘 ≠ 0 )
221	220	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ≠ 0 )
222	206, 221	eldifsnd 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
223	222	an72ds 32713	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
224		oveq2 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑘 → (𝑦 · 𝑧) = (𝑦 · 𝑘))
225	224	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑘 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
226	225	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
227		eleq1w 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (𝑧 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆))
228	226, 227	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑘 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
229	228	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑧 = 𝑘) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
230	223, 229	rspcdv 3576	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
231	230	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
232	231	an82ds 32714	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
233	203, 232	mpd 16	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑆)
234		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑝 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g 𝑓)))
235	234	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑝 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓)))
236		oveq2 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑝”⟩))
237	236	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑝 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩)))
238		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
239	238	s1cld 14631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ⟨“𝑝”⟩ ∈ Word 𝑃)
240	89	gsumws1 18887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑝 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
241	211, 240	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
242	241	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩))
243	237, 239, 242	rspcedvdw 3587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓))
244	235, 211, 243	elrabd 3655	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
245	244, 173	eleqtrrdi 2876	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑆)
246	245	ad7antr 750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑆)
247	56, 176, 51, 74, 45, 178, 181, 173, 55, 233, 246	1arithufdlem2 33752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑆)
248	175, 247	eqeltrrd 2866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑆)
249	174, 248	pm2.61dan 824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
250	249	r19.29an 3169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
251	250	adantrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡)) → 𝑡 ∈ 𝑆)
252	153, 251	sylan2b 605	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑡) → 𝑡 ∈ 𝑆)
253		simplr 780	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑤 ∈ 𝐵)
254	56, 68, 55	dvdsrmul 20437	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ 𝐵 ∧ (𝑀 Σ_g 𝑑) ∈ 𝐵) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
255	82, 105, 254	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
256	255, 124	breqtrrd 5133	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)(𝑤 · 𝑡))
257	56, 74, 68, 55, 84, 81, 253, 110, 256	rprmdvds 33726	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑝(∥_r‘𝑅)𝑤 ∨ 𝑝(∥_r‘𝑅)𝑡))
258	152, 252, 257	mpjaodan 973	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
259	258	r19.29an 3169	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
260	67, 259	sylan2b 605	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
261	260	ex 417	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
262	261	ralrimiva 3157	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → ∀𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
263	140	eqeq1d 2767	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
264	263	rexbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
265	264, 143	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆)))
266	265	cbvralvw 3243	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆) ↔ ∀𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
267	262, 266	sylibr 237	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))
268	267	ex 417	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
269	268	anasss 471	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃)) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
270	269	expcom 418	. . . . . . . 8 ⊢ ((𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝜑 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
271	270	a2d 30	. . . . . . 7 ⊢ ((𝑑 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃) → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
272	17, 23, 29, 35, 64, 271	wrdind 14749	. . . . . 6 ⊢ (𝑓 ∈ Word 𝑃 → (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
273	272	impcom 412	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))
274		1arithufdlem.3	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
275		1arithufdlem.4	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
276	274, 275	eldifd 3918	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈))
277		1arithufdlem.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ≠ 0 )
278	276, 277	eldifsnd 4750	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
279	278	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
280	11, 273, 279	rspcdva 3585	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆))
281	280	imp 411	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
282	6, 281	syldan 602	. 2 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
283		1arithufdlem3.1	. . . . 5 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)
284	283, 173	eleqtrdi 2875	. . . 4 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
285		eqeq1 2769	. . . . . 6 ⊢ (𝑥 = (𝑌 · 𝑋) → (𝑥 = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
286	285	rexbidv 3189	. . . . 5 ⊢ (𝑥 = (𝑌 · 𝑋) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
287	286	elrab 3653	. . . 4 ⊢ ((𝑌 · 𝑋) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)} ↔ ((𝑌 · 𝑋) ∈ 𝐵 ∧ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
288	284, 287	sylib 221	. . 3 ⊢ (𝜑 → ((𝑌 · 𝑋) ∈ 𝐵 ∧ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
289	288	simprd 500	. 2 ⊢ (𝜑 → ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓))
290	282, 289	r19.29a 3173	1 ⊢ (𝜑 → 𝑋 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∀wral 3079 ∃wrex 3089 {crab 3417 Vcvv 3457 ∖ cdif 3904 ⊆ wss 3907 ∅c0 4288 {csn 4585 class class class wbr 5105 ‘cfv 6525 (class class class)co 7400 0cc0 11088 ..^cfzo 13673 ♯chash 14357 Word cword 14540 ++ cconcat 14597 ⟨“cs1 14623 Basecbs 17259 ._rcmulr 17301 0_gc0g 17482 Σ_g cgsu 17483 Mndcmnd 18782 CMndccmn 19841 mulGrpcmgp 20207 1_rcur 20254 Ringcrg 20306 CRingccrg 20307 ∥_rcdsr 20427 Unitcui 20428 RPrimecrpm 20505 Domncdomn 20768 IDomncidom 20769 DivRingcdr 20804 UFDcufd 33745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-se 5606 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-supp 8145 df-tpos 8210 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fsupp 9310 df-oi 9460 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-n0 12496 df-xnn0 12569 df-z 12583 df-uz 12854 df-fz 13527 df-fzo 13674 df-seq 14029 df-hash 14358 df-word 14541 df-lsw 14590 df-concat 14598 df-s1 14624 df-substr 14669 df-pfx 14699 df-sets 17214 df-slot 17232 df-ndx 17244 df-base 17260 df-ress 17281 df-plusg 17313 df-mulr 17314 df-sca 17316 df-vsca 17317 df-ip 17318 df-0g 17484 df-gsum 17485 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-submnd 18832 df-grp 18993 df-minusg 18994 df-sbg 18995 df-subg 19180 df-cntz 19378 df-cmn 19843 df-abl 19844 df-mgp 20208 df-rng 20222 df-ur 20255 df-ring 20308 df-cring 20309 df-oppr 20410 df-dvdsr 20430 df-unit 20431 df-invr 20461 df-rprm 20506 df-nzr 20587 df-subrg 20646 df-domn 20771 df-idom 20772 df-lmod 20952 df-lss 21022 df-lsp 21062 df-sra 21263 df-rgmod 21264 df-lidl 21301 df-rsp 21302 df-prmidl 21423 df-ufd 33746

This theorem is referenced by: 1arithufdlem4 33754

W3C validator