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	$⊢ B = {Base}_{R}$
	1arithufd.0	$⊢ \underset{˙}{0} = 0_{R}$
	1arithufd.u	$⊢ U = Unit (R)$
	1arithufd.p	$⊢ P = RPrime (R)$
	1arithufd.m	$⊢ M = {mulGrp}_{R}$
	1arithufd.r	$⊢ φ \to R \in UFD$
	1arithufd.x	$⊢ φ \to X \in B$
	1arithufd.2	$⊢ φ \to \neg X \in U$
	1arithufd.3	$⊢ φ \to X \neq \underset{˙}{0}$
Assertion	1arithufd	$⊢ φ \to \exists f \in Word P X = \sum_{M} f$

Proof

Step	Hyp	Ref	Expression
1		1arithufd.b	$⊢ B = {Base}_{R}$
2		1arithufd.0	$⊢ \underset{˙}{0} = 0_{R}$
3		1arithufd.u	$⊢ U = Unit (R)$
4		1arithufd.p	$⊢ P = RPrime (R)$
5		1arithufd.m	$⊢ M = {mulGrp}_{R}$
6		1arithufd.r	$⊢ φ \to R \in UFD$
7		1arithufd.x	$⊢ φ \to X \in B$
8		1arithufd.2	$⊢ φ \to \neg X \in U$
9		1arithufd.3	$⊢ φ \to X \neq \underset{˙}{0}$
10		simpr	$⊢ (φ \land R \in DivRing) \to R \in DivRing$
11	7	adantr	$⊢ (φ \land R \in DivRing) \to X \in B$
12	9	adantr	$⊢ (φ \land R \in DivRing) \to X \neq \underset{˙}{0}$
13	1 3 2	drngunit	$⊢ R \in DivRing \to (X \in U \leftrightarrow (X \in B \land X \neq \underset{˙}{0}))$
14	13	biimpar	$⊢ (R \in DivRing \land (X \in B \land X \neq \underset{˙}{0})) \to X \in U$
15	10 11 12 14	syl12anc	$⊢ (φ \land R \in DivRing) \to X \in U$
16	8	adantr	$⊢ (φ \land R \in DivRing) \to \neg X \in U$
17	15 16	pm2.21dd	$⊢ (φ \land R \in DivRing) \to \exists f \in Word P X = \sum_{M} f$
18	6	adantr	$⊢ (φ \land \neg R \in DivRing) \to R \in UFD$
19		simpr	$⊢ (φ \land \neg R \in DivRing) \to \neg R \in DivRing$
20		eqeq1	$⊢ y = x \to (y = \sum_{M} f \leftrightarrow x = \sum_{M} f)$
21	20	rexbidv	$⊢ y = x \to (\exists f \in Word P y = \sum_{M} f \leftrightarrow \exists f \in Word P x = \sum_{M} f)$
22	21	cbvrabv	$⊢ \{y \in B \| \exists f \in Word P y = \sum_{M} f\} = \{x \in B \| \exists f \in Word P x = \sum_{M} f\}$
23		oveq2	$⊢ f = g \to \sum_{M} f = \sum_{M} g$
24	23	eqeq2d	$⊢ f = g \to (x = \sum_{M} f \leftrightarrow x = \sum_{M} g)$
25	24	cbvrexvw	$⊢ \exists f \in Word P x = \sum_{M} f \leftrightarrow \exists g \in Word P x = \sum_{M} g$
26	22 25	rabbieq	$⊢ \{y \in B \| \exists f \in Word P y = \sum_{M} f\} = \{x \in B \| \exists g \in Word P x = \sum_{M} g\}$
27	7	adantr	$⊢ (φ \land \neg R \in DivRing) \to X \in B$
28	8	adantr	$⊢ (φ \land \neg R \in DivRing) \to \neg X \in U$
29	9	adantr	$⊢ (φ \land \neg R \in DivRing) \to X \neq \underset{˙}{0}$
30	1 2 3 4 5 18 19 26 27 28 29	1arithufdlem4	$⊢ (φ \land \neg R \in DivRing) \to X \in \{y \in B \| \exists f \in Word P y = \sum_{M} f\}$
31		eqeq1	$⊢ y = X \to (y = \sum_{M} f \leftrightarrow X = \sum_{M} f)$
32	31	rexbidv	$⊢ y = X \to (\exists f \in Word P y = \sum_{M} f \leftrightarrow \exists f \in Word P X = \sum_{M} f)$
33	32	elrab	$⊢ X \in \{y \in B \| \exists f \in Word P y = \sum_{M} f\} \leftrightarrow (X \in B \land \exists f \in Word P X = \sum_{M} f)$
34	30 33	sylib	$⊢ (φ \land \neg R \in DivRing) \to (X \in B \land \exists f \in Word P X = \sum_{M} f)$
35	34	simprd	$⊢ (φ \land \neg R \in DivRing) \to \exists f \in Word P X = \sum_{M} f$
36	17 35	pm2.61dan	$⊢ φ \to \exists f \in Word P X = \sum_{M} f$

Metamath Proof Explorer

Theorem 1arithufd

Proof