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 33517

Description: Lemma for 1arithufd 33519. 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 7394	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑦 · 𝑋) = (𝑌 · 𝑋))
2	1	eqeq1d 2731	. . . 4 ⊢ (𝑦 = 𝑌 → ((𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
3		1arithufdlem3.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4	3	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑌 ∈ 𝐵)
5		simpr 484	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓))
6	2, 4, 5	rspcedvdw 3591	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓))
7		oveq2 7395	. . . . . . . 8 ⊢ (𝑧 = 𝑋 → (𝑦 · 𝑧) = (𝑦 · 𝑋))
8	7	eqeq1d 2731	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
9	8	rexbidv 3157	. . . . . 6 ⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)))
10		eleq1 2816	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑧 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆))
11	9, 10	imbi12d 344	. . . . 5 ⊢ (𝑧 = 𝑋 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆)))
12		oveq2 7395	. . . . . . . . . . . 12 ⊢ (𝑐 = ∅ → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g ∅))
13	12	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
14	13	rexbidv 3157	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)))
15	14	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
16	15	ralbidv 3156	. . . . . . . 8 ⊢ (𝑐 = ∅ → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆)))
17	16	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))))
18		oveq2 7395	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑑 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑑))
19	18	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑑 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
20	19	rexbidv 3157	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑)))
21	20	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
22	21	ralbidv 3156	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)))
23	22	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆))))
24		oveq2 7395	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
25	24	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
26	25	rexbidv 3157	. . . . . . . . . 10 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
27	26	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
28	27	ralbidv 3156	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆)))
29	28	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑝”⟩) → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆))))
30		oveq2 7395	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑓 → (𝑀 Σ_g 𝑐) = (𝑀 Σ_g 𝑓))
31	30	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑓 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
32	31	rexbidv 3157	. . . . . . . . . 10 ⊢ (𝑐 = 𝑓 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓)))
33	32	imbi1d 341	. . . . . . . . 9 ⊢ (𝑐 = 𝑓 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
34	33	ralbidv 3156	. . . . . . . 8 ⊢ (𝑐 = 𝑓 → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆) ↔ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
35	34	imbi2d 340	. . . . . . 7 ⊢ (𝑐 = 𝑓 → ((𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑐) → 𝑧 ∈ 𝑆)) ↔ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))))
36		1arithufd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ UFD)
37	36	ufdidom 33513	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ IDomn)
38	37	idomcringd 20636	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ CRing)
39	38	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ CRing)
40		simpllr 775	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝐵)
41		simp-4r 783	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
42	41	eldifad 3926	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ (𝐵 ∖ 𝑈))
43	42	eldifad 3926	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐵)
44		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (𝑀 Σ_g ∅))
45		1arithufd.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (mulGrp‘𝑅)
46		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
47	45, 46	ringidval 20092	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝑅) = (0_g‘𝑀)
48	47	gsum0 18611	. . . . . . . . . . . . . 14 ⊢ (𝑀 Σ_g ∅) = (1_r‘𝑅)
49	44, 48	eqtrdi 2780	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (1_r‘𝑅))
50	39	crngringd 20155	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑅 ∈ Ring)
51		1arithufd.u	. . . . . . . . . . . . . . 15 ⊢ 𝑈 = (Unit‘𝑅)
52	51, 46	1unit 20283	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝑈)
53	50, 52	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (1_r‘𝑅) ∈ 𝑈)
54	49, 53	eqeltrd 2828	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) ∈ 𝑈)
55		1arithufdlem3.p	. . . . . . . . . . . . . 14 ⊢ · = (._r‘𝑅)
56		1arithufd.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝑅)
57	51, 55, 56	unitmulclb 20290	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑦 · 𝑧) ∈ 𝑈 ↔ (𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)))
58	57	simplbda 499	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑦 · 𝑧) ∈ 𝑈) → 𝑧 ∈ 𝑈)
59	39, 40, 43, 54, 58	syl31anc 1375	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑈)
60	42	eldifbd 3927	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) ∧ ¬ 𝑧 ∈ 𝑆) → ¬ 𝑧 ∈ 𝑈)
61	59, 60	condan 817	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
62	61	r19.29an 3137	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅)) → 𝑧 ∈ 𝑆)
63	62	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
64	63	ralrimiva 3125	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g ∅) → 𝑧 ∈ 𝑆))
65		oveq1 7394	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑡) = (𝑤 · 𝑡))
66	65	eqeq1d 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → ((𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
67	66	cbvrexvw 3216	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
68		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (∥_r‘𝑅) = (∥_r‘𝑅)
69	56, 68, 55	dvdsr 20271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑤 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤))
70		oveq1 7394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑘 → (𝑣 · 𝑡) = (𝑘 · 𝑡))
71	70	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑘 → ((𝑣 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑)))
72		simplr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑘 ∈ 𝐵)
73		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 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 33489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
78	77	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝑝 ∈ 𝑃 → 𝑝 ∈ 𝐵))
79	78	ssrdv 3952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑃 ⊆ 𝐵)
80	79	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑃 ⊆ 𝐵)
81		simp-5r 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝑃)
82	80, 81	sseldd 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝 ∈ 𝐵)
83	82	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝐵)
84	36	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑅 ∈ UFD)
85	84	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ UFD)
86	81	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ 𝑃)
87	74, 73, 85, 86	rprmnz 33491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ≠ (0_g‘𝑅))
88	83, 87	eldifsnd 4751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑝 ∈ (𝐵 ∖ {(0_g‘𝑅)}))
89	45, 56	mgpbas 20054	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐵 = (Base‘𝑀)
90	45	crngmgp 20150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ CRing → 𝑀 ∈ CMnd)
91	38, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑀 ∈ CMnd)
92	91	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ CMnd)
93		ovexd 7422	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (0..^(♯‘𝑑)) ∈ V)
94		eqidd 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (♯‘𝑑) = (♯‘𝑑))
95		sswrd 14487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ⊆ 𝐵 → Word 𝑃 ⊆ Word 𝐵)
96	79, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → Word 𝑃 ⊆ Word 𝐵)
97	96	sselda 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑑 ∈ Word 𝑃) → 𝑑 ∈ Word 𝐵)
98	97	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝐵)
99	94, 98	wrdfd 14484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑:(0..^(♯‘𝑑))⟶𝐵)
100	38	crngringd 20155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑅 ∈ Ring)
101	100, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝑈)
102	101	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (1_r‘𝑅) ∈ 𝑈)
103		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 ∈ Word 𝑃)
104	102, 103	wrdfsupp 32858	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑑 finSupp (1_r‘𝑅))
105	89, 47, 92, 93, 99, 104	gsumcl 19845	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
106	105	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
107	100	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Ring)
108		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
109	108	eldifad 3926	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ (𝐵 ∖ 𝑈))
110	109	eldifad 3926	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝐵)
111	110	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝐵)
112	56, 55, 107, 72, 111	ringcld 20169	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) ∈ 𝐵)
113	37	idomdomd 20635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ∈ Domn)
114	113	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ Domn)
115	38	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑅 ∈ CRing)
116	56, 55, 115, 83, 106	crngcomd 20164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = ((𝑀 Σ_g 𝑑) · 𝑝))
117		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)))
118	45	ringmgp 20148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
119	100, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ Mnd)
120	119	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑀 ∈ Mnd)
121	45, 55	mgpplusg 20053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ · = (+_g‘𝑀)
122	89, 121	gsumccatsn 18770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ Mnd ∧ 𝑑 ∈ Word 𝐵 ∧ 𝑝 ∈ 𝐵) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
123	120, 98, 82, 122	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) = ((𝑀 Σ_g 𝑑) · 𝑝))
124	117, 123	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
125	124	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
126	56, 55, 107, 72, 83, 111	ringassd 20166	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑘 · (𝑝 · 𝑡)))
127		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑝) = 𝑤)
128	127	oveq1d 7402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ((𝑘 · 𝑝) · 𝑡) = (𝑤 · 𝑡))
129	56, 55, 115, 72, 83, 111	crng12d 20167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · (𝑝 · 𝑡)) = (𝑝 · (𝑘 · 𝑡)))
130	126, 128, 129	3eqtr3d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑤 · 𝑡) = (𝑝 · (𝑘 · 𝑡)))
131	116, 125, 130	3eqtr2d 2770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑝 · (𝑀 Σ_g 𝑑)) = (𝑝 · (𝑘 · 𝑡)))
132	56, 73, 55, 88, 106, 112, 114, 131	domnlcan 20630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑀 Σ_g 𝑑) = (𝑘 · 𝑡))
133	132	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (𝑘 · 𝑡) = (𝑀 Σ_g 𝑑))
134	71, 72, 133	rspcedvdw 3591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
135		oveq1 7394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑡) = (𝑣 · 𝑡))
136	135	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑)))
137	136	cbvrexvw 3216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) ↔ ∃𝑣 ∈ 𝐵 (𝑣 · 𝑡) = (𝑀 Σ_g 𝑑))
138	134, 137	sylibr 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑))
139		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
140		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑡 → (𝑦 · 𝑧) = (𝑦 · 𝑡))
141	140	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
142	141	rexbidv 3157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑)))
143		eleq1w 2811	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑆 ↔ 𝑡 ∈ 𝑆))
144	142, 143	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
145	144	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = 𝑡) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
146	139, 145	rspcdv 3580	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆)))
147	146	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑤) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
148	147	an72ds 32382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g 𝑑) → 𝑡 ∈ 𝑆))
149	138, 148	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
150	149	r19.29an 3137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤) → 𝑡 ∈ 𝑆)
151	150	adantrl 716	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑤)) → 𝑡 ∈ 𝑆)
152	69, 151	sylan2b 594	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑤) → 𝑡 ∈ 𝑆)
153	56, 68, 55	dvdsr 20271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(∥_r‘𝑅)𝑡 ↔ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡))
154		eqeq1 2733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g 𝑓)))
155	154	rexbidv 3157	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑡 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓)))
156	110	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝐵)
157		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑡”⟩))
158	157	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ⟨“𝑡”⟩ → (𝑡 = (𝑀 Σ_g 𝑓) ↔ 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩)))
159		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
160	37	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ IDomn)
161	160	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑅 ∈ IDomn)
162		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑈)
163	81	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝑃)
164	163	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑃)
165	74, 51, 55, 161, 162, 164	unitmulrprm 33499	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑃)
166	159, 165	eqeltrrd 2829	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑃)
167	166	s1cld 14568	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ⟨“𝑡”⟩ ∈ Word 𝑃)
168	89	gsumws1 18765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑡”⟩) = 𝑡)
169	156, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → (𝑀 Σ_g ⟨“𝑡”⟩) = 𝑡)
170	169	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 = (𝑀 Σ_g ⟨“𝑡”⟩))
171	158, 167, 170	rspcedvdw 3591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → ∃𝑓 ∈ Word 𝑃𝑡 = (𝑀 Σ_g 𝑓))
172	155, 156, 171	elrabd 3661	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
173		1arithufdlem.s	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)}
174	172, 173	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑆)
175		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) = 𝑡)
176		1arithufd.0	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 = (0_g‘𝑅)
177	84	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ UFD)
178	177	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑅 ∈ UFD)
179		1arithufdlem.2	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑅 ∈ DivRing)
180	179	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ¬ 𝑅 ∈ DivRing)
181	180	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑅 ∈ DivRing)
182		oveq1 7394	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑤 → (𝑣 · 𝑘) = (𝑤 · 𝑘))
183	182	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → ((𝑣 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑)))
184		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑤 ∈ 𝐵)
185	100	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑅 ∈ Ring)
186		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ 𝐵)
187	56, 55, 185, 184, 186	ringcld 20169	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) ∈ 𝐵)
188	105	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑀 Σ_g 𝑑) ∈ 𝐵)
189	82	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ 𝐵)
190	74, 176, 177, 163	rprmnz 33491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ≠ 0 )
191	189, 190	eldifsnd 4751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑝 ∈ (𝐵 ∖ { 0 }))
192	56, 55, 185, 184, 186, 189	ringassd 20166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = (𝑤 · (𝑘 · 𝑝)))
193		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑘 · 𝑝) = 𝑡)
194	193	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · (𝑘 · 𝑝)) = (𝑤 · 𝑡))
195	124	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑡) = ((𝑀 Σ_g 𝑑) · 𝑝))
196	192, 194, 195	3eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ((𝑤 · 𝑘) · 𝑝) = ((𝑀 Σ_g 𝑑) · 𝑝))
197	56, 176, 55, 187, 188, 191, 160, 196	idomrcan 33229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (𝑤 · 𝑘) = (𝑀 Σ_g 𝑑))
198	183, 184, 197	rspcedvdw 3591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → ∃𝑣 ∈ 𝐵 (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑))
199		oveq1 7394	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑣 → (𝑦 · 𝑘) = (𝑣 · 𝑘))
200	199	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑣 → ((𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) ↔ (𝑣 · 𝑘) = (𝑀 Σ_g 𝑑)))
201	200	cbvrexvw 3216	. . . . . . . . . . . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝐵)
205		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → ¬ 𝑘 ∈ 𝑈)
206	204, 205	eldifd 3925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ (𝐵 ∖ 𝑈))
207		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
208	207	oveq1d 7402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = ( 0 · 𝑝))
209		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → (𝑘 · 𝑝) = 𝑡)
210	100	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑅 ∈ Ring)
211	77	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝐵)
212	211	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑝 ∈ 𝐵)
213	56, 55, 176, 210, 212	ringlzd 20204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ( 0 · 𝑝) = 0 )
214	208, 209, 213	3eqtr3d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 = 0 )
215		simp-5r 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
216		eldifsni 4754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }) → 𝑡 ≠ 0 )
217	215, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → 𝑡 ≠ 0 )
218	217	neneqd 2930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 = 0 ) → ¬ 𝑡 = 0 )
219	214, 218	pm2.65da 816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 = 0 )
220	219	neqned 2932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) → 𝑘 ≠ 0 )
221	220	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ≠ 0 )
222	206, 221	eldifsnd 4751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
223	222	an72ds 32382	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑘 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
224		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = 𝑘 → (𝑦 · 𝑧) = (𝑦 · 𝑘))
225	224	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = 𝑘 → ((𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
226	225	rexbidv 3157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑)))
227		eleq1w 2811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = 𝑘 → (𝑧 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆))
228	226, 227	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = 𝑘 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
229	228	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ 𝑧 = 𝑘) → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
230	223, 229	rspcdv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → (∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆)))
231	230	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ¬ 𝑘 ∈ 𝑈) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
232	231	an82ds 32383	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑘) = (𝑀 Σ_g 𝑑) → 𝑘 ∈ 𝑆))
233	203, 232	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑆)
234		eqeq1 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑝 → (𝑥 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g 𝑓)))
235	234	rexbidv 3157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑝 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓)))
236		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑀 Σ_g 𝑓) = (𝑀 Σ_g ⟨“𝑝”⟩))
237	236	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = ⟨“𝑝”⟩ → (𝑝 = (𝑀 Σ_g 𝑓) ↔ 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩)))
238		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
239	238	s1cld 14568	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ⟨“𝑝”⟩ ∈ Word 𝑃)
240	89	gsumws1 18765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑝 ∈ 𝐵 → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
241	211, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → (𝑀 Σ_g ⟨“𝑝”⟩) = 𝑝)
242	241	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 = (𝑀 Σ_g ⟨“𝑝”⟩))
243	237, 239, 242	rspcedvdw 3591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → ∃𝑓 ∈ Word 𝑃𝑝 = (𝑀 Σ_g 𝑓))
244	235, 211, 243	elrabd 3661	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
245	244, 173	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑆)
246	245	ad7antr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑝 ∈ 𝑆)
247	56, 176, 51, 74, 45, 178, 181, 173, 55, 233, 246	1arithufdlem2 33516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → (𝑘 · 𝑝) ∈ 𝑆)
248	175, 247	eqeltrrd 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) ∧ ¬ 𝑘 ∈ 𝑈) → 𝑡 ∈ 𝑆)
249	174, 248	pm2.61dan 812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑘 ∈ 𝐵) ∧ (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
250	249	r19.29an 3137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡) → 𝑡 ∈ 𝑆)
251	250	adantrl 716	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ (𝑝 ∈ 𝐵 ∧ ∃𝑘 ∈ 𝐵 (𝑘 · 𝑝) = 𝑡)) → 𝑡 ∈ 𝑆)
252	153, 251	sylan2b 594	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) ∧ 𝑝(∥_r‘𝑅)𝑡) → 𝑡 ∈ 𝑆)
253		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑤 ∈ 𝐵)
254	56, 68, 55	dvdsrmul 20273	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ 𝐵 ∧ (𝑀 Σ_g 𝑑) ∈ 𝐵) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
255	82, 105, 254	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)((𝑀 Σ_g 𝑑) · 𝑝))
256	255, 124	breqtrrd 5135	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑝(∥_r‘𝑅)(𝑤 · 𝑡))
257	56, 74, 68, 55, 84, 81, 253, 110, 256	rprmdvds 33490	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → (𝑝(∥_r‘𝑅)𝑤 ∨ 𝑝(∥_r‘𝑅)𝑡))
258	152, 252, 257	mpjaodan 960	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ 𝑤 ∈ 𝐵) ∧ (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
259	258	r19.29an 3137	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑤 ∈ 𝐵 (𝑤 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
260	67, 259	sylan2b 594	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))) → 𝑡 ∈ 𝑆)
261	260	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) ∧ 𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
262	261	ralrimiva 3125	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑑 ∈ Word 𝑃) ∧ 𝑝 ∈ 𝑃) ∧ ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑑) → 𝑧 ∈ 𝑆)) → ∀𝑡 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆))
263	140	eqeq1d 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑡 → ((𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
264	263	rexbidv 3157	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑡 → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩))))
265	264, 143	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑡 → ((∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑧 ∈ 𝑆) ↔ (∃𝑦 ∈ 𝐵 (𝑦 · 𝑡) = (𝑀 Σ_g (𝑑 ++ ⟨“𝑝”⟩)) → 𝑡 ∈ 𝑆)))
266	265	cbvralvw 3215	. . . . . . . . . . . 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 14687	. . . . . 6 ⊢ (𝑓 ∈ Word 𝑃 → (𝜑 → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆)))
273	272	impcom 407	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → ∀𝑧 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })(∃𝑦 ∈ 𝐵 (𝑦 · 𝑧) = (𝑀 Σ_g 𝑓) → 𝑧 ∈ 𝑆))
274		1arithufdlem.3	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
275		1arithufdlem.4	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
276	274, 275	eldifd 3925	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑈))
277		1arithufdlem.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ≠ 0 )
278	276, 277	eldifsnd 4751	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
279	278	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → 𝑋 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
280	11, 273, 279	rspcdva 3589	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ Word 𝑃) → (∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓) → 𝑋 ∈ 𝑆))
281	280	imp 406	. . 3 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
282	6, 281	syldan 591	. 2 ⊢ (((𝜑 ∧ 𝑓 ∈ Word 𝑃) ∧ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)) → 𝑋 ∈ 𝑆)
283		1arithufdlem3.1	. . . . 5 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ 𝑆)
284	283, 173	eleqtrdi 2838	. . . 4 ⊢ (𝜑 → (𝑌 · 𝑋) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓)})
285		eqeq1 2733	. . . . . 6 ⊢ (𝑥 = (𝑌 · 𝑋) → (𝑥 = (𝑀 Σ_g 𝑓) ↔ (𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
286	285	rexbidv 3157	. . . . 5 ⊢ (𝑥 = (𝑌 · 𝑋) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σ_g 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑌 · 𝑋) = (𝑀 Σ_g 𝑓)))
287	286	elrab 3659	. . . 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 3141	1 ⊢ (𝜑 → 𝑋 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3405 Vcvv 3447 ∖ cdif 3911 ⊆ wss 3914 ∅c0 4296 {csn 4589 class class class wbr 5107 ‘cfv 6511 (class class class)co 7387 0cc0 11068 ..^cfzo 13615 ♯chash 14295 Word cword 14478 ++ cconcat 14535 ⟨“cs1 14560 Basecbs 17179 ._rcmulr 17221 0_gc0g 17402 Σ_g cgsu 17403 Mndcmnd 18661 CMndccmn 19710 mulGrpcmgp 20049 1_rcur 20090 Ringcrg 20142 CRingccrg 20143 ∥_rcdsr 20263 Unitcui 20264 RPrimecrpm 20341 Domncdomn 20601 IDomncidom 20602 DivRingcdr 20638 UFDcufd 33509

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-tpos 8205 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-n0 12443 df-xnn0 12516 df-z 12530 df-uz 12794 df-fz 13469 df-fzo 13616 df-seq 13967 df-hash 14296 df-word 14479 df-lsw 14528 df-concat 14536 df-s1 14561 df-substr 14606 df-pfx 14636 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-sca 17236 df-vsca 17237 df-ip 17238 df-0g 17404 df-gsum 17405 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-grp 18868 df-minusg 18869 df-sbg 18870 df-subg 19055 df-cntz 19249 df-cmn 19712 df-abl 19713 df-mgp 20050 df-rng 20062 df-ur 20091 df-ring 20144 df-cring 20145 df-oppr 20246 df-dvdsr 20266 df-unit 20267 df-invr 20297 df-rprm 20342 df-nzr 20422 df-subrg 20479 df-domn 20604 df-idom 20605 df-lmod 20768 df-lss 20838 df-lsp 20878 df-sra 21080 df-rgmod 21081 df-lidl 21118 df-rsp 21119 df-prmidl 33407 df-ufd 33510

This theorem is referenced by: 1arithufdlem4 33518

W3C validator