Theorem 1arithufdlem3

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

	Ref	Expression
Hypotheses	1arithufd.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	1arithufd.0	⊢ 0 = ( 0g ‘ 𝑅 )
	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	1arithufdlem3	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )

Proof

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