Theorem 1arithufdlem1

Description: Lemma for 1arithufd . The set S of elements which can be written as a product of primes is not empty. (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 𝑓 ) }
Assertion	1arithufdlem1	⊢ ( 𝜑 → 𝑆 ≠ ∅ )

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		eqeq1	⊢ ( 𝑥 = 𝑝 → ( 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ 𝑝 = ( 𝑀 Σg 𝑓 ) ) )
10	9	rexbidv	⊢ ( 𝑥 = 𝑝 → ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 𝑝 = ( 𝑀 Σg 𝑓 ) ) )
11	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) → 𝑅 ∈ UFD )
12	11	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → 𝑅 ∈ UFD )
13		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → 𝑝 ∈ 𝑃 )
14	1 4 12 13	rprmcl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → 𝑝 ∈ 𝐵 )
15		oveq2	⊢ ( 𝑓 = ⟨“ 𝑝 ”⟩ → ( 𝑀 Σg 𝑓 ) = ( 𝑀 Σg ⟨“ 𝑝 ”⟩ ) )
16	15	eqeq2d	⊢ ( 𝑓 = ⟨“ 𝑝 ”⟩ → ( 𝑝 = ( 𝑀 Σg 𝑓 ) ↔ 𝑝 = ( 𝑀 Σg ⟨“ 𝑝 ”⟩ ) ) )
17	13	s1cld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → ⟨“ 𝑝 ”⟩ ∈ Word 𝑃 )
18	5 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
19	18	gsumws1	⊢ ( 𝑝 ∈ 𝐵 → ( 𝑀 Σg ⟨“ 𝑝 ”⟩ ) = 𝑝 )
20	14 19	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → ( 𝑀 Σg ⟨“ 𝑝 ”⟩ ) = 𝑝 )
21	20	eqcomd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → 𝑝 = ( 𝑀 Σg ⟨“ 𝑝 ”⟩ ) )
22	16 17 21	rspcedvdw	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → ∃ 𝑓 ∈ Word 𝑃 𝑝 = ( 𝑀 Σg 𝑓 ) )
23	10 14 22	elrabd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → 𝑝 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } )
24	23 8	eleqtrrdi	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → 𝑝 ∈ 𝑆 )
25	24	ne0d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝑚 ) → 𝑆 ≠ ∅ )
26		eqid	⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
27	6	ufdidom	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
28	27	idomcringd	⊢ ( 𝜑 → 𝑅 ∈ CRing )
29	28	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) → 𝑅 ∈ CRing )
30		simplr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
31		eqid	⊢ ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
32	31	mxidlprm	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ∈ ( PrmIdeal ‘ 𝑅 ) )
33	29 30 32	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) → 𝑚 ∈ ( PrmIdeal ‘ 𝑅 ) )
34		simpr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) → 𝑚 ≠ { 0 } )
35	26 4 2 11 33 34	ufdprmidl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) → ∃ 𝑝 ∈ 𝑃 𝑝 ∈ 𝑚 )
36	25 35	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑚 ≠ { 0 } ) → 𝑆 ≠ ∅ )
37	27	idomdomd	⊢ ( 𝜑 → 𝑅 ∈ Domn )
38		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
39	37 38	syl	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
40	2 39 7	krullndrng	⊢ ( 𝜑 → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝑚 ≠ { 0 } )
41	36 40	r19.29a	⊢ ( 𝜑 → 𝑆 ≠ ∅ )