Theorem 1arithufdlem2

Description: Lemma for 1arithufd . The set S of elements which can be written as a product of primes is multiplicatively closed. (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 𝑓 ) }
	1arithufdlem2.1	⊢ · = ( .r ‘ 𝑅 )
	1arithufdlem2.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	1arithufdlem2.3	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion	1arithufdlem2	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝑆 )

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		1arithufdlem2.1	⊢ · = ( .r ‘ 𝑅 )
10		1arithufdlem2.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
11		1arithufdlem2.3	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
12		eqeq1	⊢ ( 𝑥 = ( 𝑋 · 𝑌 ) → ( 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ( 𝑋 · 𝑌 ) = ( 𝑀 Σg 𝑓 ) ) )
13	12	rexbidv	⊢ ( 𝑥 = ( 𝑋 · 𝑌 ) → ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 ( 𝑋 · 𝑌 ) = ( 𝑀 Σg 𝑓 ) ) )
14	6	ufdidom	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
15	14	idomringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
16	8	ssrab3	⊢ 𝑆 ⊆ 𝐵
17	16 10	sselid	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
18	16 11	sselid	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
19	1 9 15 17 18	ringcld	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
20		oveq2	⊢ ( 𝑓 = ( 𝑔 ++ ℎ ) → ( 𝑀 Σg 𝑓 ) = ( 𝑀 Σg ( 𝑔 ++ ℎ ) ) )
21	20	eqeq2d	⊢ ( 𝑓 = ( 𝑔 ++ ℎ ) → ( ( 𝑋 · 𝑌 ) = ( 𝑀 Σg 𝑓 ) ↔ ( 𝑋 · 𝑌 ) = ( 𝑀 Σg ( 𝑔 ++ ℎ ) ) ) )
22		ccatcl	⊢ ( ( 𝑔 ∈ Word 𝑃 ∧ ℎ ∈ Word 𝑃 ) → ( 𝑔 ++ ℎ ) ∈ Word 𝑃 )
23	22	ad5ant24	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → ( 𝑔 ++ ℎ ) ∈ Word 𝑃 )
24		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → 𝑋 = ( 𝑀 Σg 𝑔 ) )
25		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → 𝑌 = ( 𝑀 Σg ℎ ) )
26	24 25	oveq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → ( 𝑋 · 𝑌 ) = ( ( 𝑀 Σg 𝑔 ) · ( 𝑀 Σg ℎ ) ) )
27	5	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
28	15 27	syl	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
29	28	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → 𝑀 ∈ Mnd )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑅 ∈ UFD )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑥 ∈ 𝑃 )
32	1 4 30 31	rprmcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑥 ∈ 𝐵 )
33	32	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑃 → 𝑥 ∈ 𝐵 ) )
34	33	ssrdv	⊢ ( 𝜑 → 𝑃 ⊆ 𝐵 )
35		sswrd	⊢ ( 𝑃 ⊆ 𝐵 → Word 𝑃 ⊆ Word 𝐵 )
36	34 35	syl	⊢ ( 𝜑 → Word 𝑃 ⊆ Word 𝐵 )
37	36	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → Word 𝑃 ⊆ Word 𝐵 )
38		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → 𝑔 ∈ Word 𝑃 )
39	37 38	sseldd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → 𝑔 ∈ Word 𝐵 )
40		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → ℎ ∈ Word 𝑃 )
41	37 40	sseldd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → ℎ ∈ Word 𝐵 )
42	5 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
43	5 9	mgpplusg	⊢ · = ( +g ‘ 𝑀 )
44	42 43	gsumccat	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑔 ∈ Word 𝐵 ∧ ℎ ∈ Word 𝐵 ) → ( 𝑀 Σg ( 𝑔 ++ ℎ ) ) = ( ( 𝑀 Σg 𝑔 ) · ( 𝑀 Σg ℎ ) ) )
45	29 39 41 44	syl3anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → ( 𝑀 Σg ( 𝑔 ++ ℎ ) ) = ( ( 𝑀 Σg 𝑔 ) · ( 𝑀 Σg ℎ ) ) )
46	26 45	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → ( 𝑋 · 𝑌 ) = ( 𝑀 Σg ( 𝑔 ++ ℎ ) ) )
47	21 23 46	rspcedvdw	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) ∧ ℎ ∈ Word 𝑃 ) ∧ 𝑌 = ( 𝑀 Σg ℎ ) ) → ∃ 𝑓 ∈ Word 𝑃 ( 𝑋 · 𝑌 ) = ( 𝑀 Σg 𝑓 ) )
48	11 8	eleqtrdi	⊢ ( 𝜑 → 𝑌 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } )
49		oveq2	⊢ ( 𝑓 = ℎ → ( 𝑀 Σg 𝑓 ) = ( 𝑀 Σg ℎ ) )
50	49	eqeq2d	⊢ ( 𝑓 = ℎ → ( 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ 𝑥 = ( 𝑀 Σg ℎ ) ) )
51	50	cbvrexvw	⊢ ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ ℎ ∈ Word 𝑃 𝑥 = ( 𝑀 Σg ℎ ) )
52		eqeq1	⊢ ( 𝑥 = 𝑌 → ( 𝑥 = ( 𝑀 Σg ℎ ) ↔ 𝑌 = ( 𝑀 Σg ℎ ) ) )
53	52	rexbidv	⊢ ( 𝑥 = 𝑌 → ( ∃ ℎ ∈ Word 𝑃 𝑥 = ( 𝑀 Σg ℎ ) ↔ ∃ ℎ ∈ Word 𝑃 𝑌 = ( 𝑀 Σg ℎ ) ) )
54	51 53	bitrid	⊢ ( 𝑥 = 𝑌 → ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ ℎ ∈ Word 𝑃 𝑌 = ( 𝑀 Σg ℎ ) ) )
55	54	elrab3	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑌 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } ↔ ∃ ℎ ∈ Word 𝑃 𝑌 = ( 𝑀 Σg ℎ ) ) )
56	55	biimpa	⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } ) → ∃ ℎ ∈ Word 𝑃 𝑌 = ( 𝑀 Σg ℎ ) )
57	18 48 56	syl2anc	⊢ ( 𝜑 → ∃ ℎ ∈ Word 𝑃 𝑌 = ( 𝑀 Σg ℎ ) )
58	57	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) → ∃ ℎ ∈ Word 𝑃 𝑌 = ( 𝑀 Σg ℎ ) )
59	47 58	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ Word 𝑃 ) ∧ 𝑋 = ( 𝑀 Σg 𝑔 ) ) → ∃ 𝑓 ∈ Word 𝑃 ( 𝑋 · 𝑌 ) = ( 𝑀 Σg 𝑓 ) )
60	10 8	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } )
61		oveq2	⊢ ( 𝑓 = 𝑔 → ( 𝑀 Σg 𝑓 ) = ( 𝑀 Σg 𝑔 ) )
62	61	eqeq2d	⊢ ( 𝑓 = 𝑔 → ( 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ 𝑥 = ( 𝑀 Σg 𝑔 ) ) )
63	62	cbvrexvw	⊢ ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑔 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑔 ) )
64		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( 𝑀 Σg 𝑔 ) ↔ 𝑋 = ( 𝑀 Σg 𝑔 ) ) )
65	64	rexbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑔 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑔 ) ↔ ∃ 𝑔 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑔 ) ) )
66	63 65	bitrid	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑔 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑔 ) ) )
67	66	elrab3	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } ↔ ∃ 𝑔 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑔 ) ) )
68	67	biimpa	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } ) → ∃ 𝑔 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑔 ) )
69	17 60 68	syl2anc	⊢ ( 𝜑 → ∃ 𝑔 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑔 ) )
70	59 69	r19.29a	⊢ ( 𝜑 → ∃ 𝑓 ∈ Word 𝑃 ( 𝑋 · 𝑌 ) = ( 𝑀 Σg 𝑓 ) )
71	13 19 70	elrabd	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } )
72	71 8	eleqtrrdi	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝑆 )