Theorem 1arithufd

Description: Existence of a factorization into irreducible elements in a unique factorization domain. Any nonzero, non-unit element X of a UFD R can be written as a product of primes f . As shown in 1arithidom , that factorization is unique, up to the order of the factors and multiplication by units. (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 )
	1arithufd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	1arithufd.2	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
	1arithufd.3	⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion	1arithufd	⊢ ( 𝜑 → ∃ 𝑓 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑓 ) )

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		1arithufd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		1arithufd.2	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
9		1arithufd.3	⊢ ( 𝜑 → 𝑋 ≠ 0 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ DivRing ) → 𝑅 ∈ DivRing )
11	7	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ DivRing ) → 𝑋 ∈ 𝐵 )
12	9	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ DivRing ) → 𝑋 ≠ 0 )
13	1 3 2	drngunit	⊢ ( 𝑅 ∈ DivRing → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ) )
14	13	biimpar	⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ) → 𝑋 ∈ 𝑈 )
15	10 11 12 14	syl12anc	⊢ ( ( 𝜑 ∧ 𝑅 ∈ DivRing ) → 𝑋 ∈ 𝑈 )
16	8	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ DivRing ) → ¬ 𝑋 ∈ 𝑈 )
17	15 16	pm2.21dd	⊢ ( ( 𝜑 ∧ 𝑅 ∈ DivRing ) → ∃ 𝑓 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑓 ) )
18	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ DivRing ) → 𝑅 ∈ UFD )
19		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ DivRing ) → ¬ 𝑅 ∈ DivRing )
20		eqeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( 𝑀 Σg 𝑓 ) ↔ 𝑥 = ( 𝑀 Σg 𝑓 ) ) )
21	20	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑓 ∈ Word 𝑃 𝑦 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ) )
22	21	cbvrabv	⊢ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑦 = ( 𝑀 Σg 𝑓 ) } = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) }
23		oveq2	⊢ ( 𝑓 = 𝑔 → ( 𝑀 Σg 𝑓 ) = ( 𝑀 Σg 𝑔 ) )
24	23	eqeq2d	⊢ ( 𝑓 = 𝑔 → ( 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ 𝑥 = ( 𝑀 Σg 𝑔 ) ) )
25	24	cbvrexvw	⊢ ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑔 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑔 ) )
26	22 25	rabbieq	⊢ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑦 = ( 𝑀 Σg 𝑓 ) } = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑔 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑔 ) }
27	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ DivRing ) → 𝑋 ∈ 𝐵 )
28	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ DivRing ) → ¬ 𝑋 ∈ 𝑈 )
29	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ DivRing ) → 𝑋 ≠ 0 )
30	1 2 3 4 5 18 19 26 27 28 29	1arithufdlem4	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ DivRing ) → 𝑋 ∈ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑦 = ( 𝑀 Σg 𝑓 ) } )
31		eqeq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 = ( 𝑀 Σg 𝑓 ) ↔ 𝑋 = ( 𝑀 Σg 𝑓 ) ) )
32	31	rexbidv	⊢ ( 𝑦 = 𝑋 → ( ∃ 𝑓 ∈ Word 𝑃 𝑦 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑓 ) ) )
33	32	elrab	⊢ ( 𝑋 ∈ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑦 = ( 𝑀 Σg 𝑓 ) } ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑓 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑓 ) ) )
34	30 33	sylib	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ DivRing ) → ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑓 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑓 ) ) )
35	34	simprd	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ DivRing ) → ∃ 𝑓 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑓 ) )
36	17 35	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑓 ∈ Word 𝑃 𝑋 = ( 𝑀 Σg 𝑓 ) )