pidufd

Description: Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025)

		Ref	Expression
	Hypothesis	pidufd.1	$⊢ φ \to R \in PID$
	Assertion	pidufd	$⊢ φ \to R \in UFD$

Proof

Step	Hyp	Ref	Expression
1		pidufd.1	$⊢ φ \to R \in PID$
2		df-pid	$⊢ PID = IDomn \cap LPIR$
3	1 2	eleqtrdi	$⊢ φ \to R \in (IDomn \cap LPIR)$
4	3	elin1d	$⊢ φ \to R \in IDomn$
5	4	idomringd	$⊢ φ \to R \in Ring$
6	5	ad3antrrr	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to R \in Ring$
7		simplr	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to x \in {Base}_{R}$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ RSpan (R) = RSpan (R)$
10	8 9	rspsnid	$⊢ (R \in Ring \land x \in {Base}_{R}) \to x \in RSpan (R) (\{x\})$
11	6 7 10	syl2anc	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to x \in RSpan (R) (\{x\})$
12		simpr	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to i = RSpan (R) (\{x\})$
13	11 12	eleqtrrd	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to x \in i$
14		simpr	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})$
15	14	eldifad	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to i \in PrmIdeal (R)$
16	15	ad2antrr	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to i \in PrmIdeal (R)$
17	12 16	eqeltrrd	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to RSpan (R) (\{x\}) \in PrmIdeal (R)$
18		eqid	$⊢ 0_{R} = 0_{R}$
19		eqid	$⊢ RPrime (R) = RPrime (R)$
20	4	ad3antrrr	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to R \in IDomn$
21	20	idomcringd	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to R \in CRing$
22		simplr	$⊢ ((((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \land x = 0_{R}) \to i = RSpan (R) (\{x\})$
23		simpr	$⊢ ((((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \land x = 0_{R}) \to x = 0_{R}$
24	23	sneqd	$⊢ ((((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \land x = 0_{R}) \to \{x\} = \{0_{R}\}$
25	24	fveq2d	$⊢ ((((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \land x = 0_{R}) \to RSpan (R) (\{x\}) = RSpan (R) (\{0_{R}\})$
26	9 18	rsp0	$⊢ R \in Ring \to RSpan (R) (\{0_{R}\}) = \{0_{R}\}$
27	5 26	syl	$⊢ φ \to RSpan (R) (\{0_{R}\}) = \{0_{R}\}$
28	27	ad4antr	$⊢ ((((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \land x = 0_{R}) \to RSpan (R) (\{0_{R}\}) = \{0_{R}\}$
29	22 25 28	3eqtrd	$⊢ ((((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \land x = 0_{R}) \to i = \{0_{R}\}$
30		eldifsni	$⊢ i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\}) \to i \neq \{0_{R}\}$
31	30	ad4antlr	$⊢ ((((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \land x = 0_{R}) \to i \neq \{0_{R}\}$
32	31	neneqd	$⊢ ((((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \land x = 0_{R}) \to \neg i = \{0_{R}\}$
33	29 32	pm2.65da	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to \neg x = 0_{R}$
34	33	neqned	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to x \neq 0_{R}$
35	18 8 19 9 21 7 34	rsprprmprmidlb	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to (x \in RPrime (R) \leftrightarrow RSpan (R) (\{x\}) \in PrmIdeal (R))$
36	17 35	mpbird	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to x \in RPrime (R)$
37	13 36	elind	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to x \in (i \cap RPrime (R))$
38	37	ne0d	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to i \cap RPrime (R) \neq \emptyset$
39		eqid	$⊢ LIdeal (R) = LIdeal (R)$
40	3	elin2d	$⊢ φ \to R \in LPIR$
41	40	adantr	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to R \in LPIR$
42	5	adantr	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to R \in Ring$
43		prmidlidl	$⊢ (R \in Ring \land i \in PrmIdeal (R)) \to i \in LIdeal (R)$
44	42 15 43	syl2anc	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to i \in LIdeal (R)$
45	8 39 9 41 44	lpirlidllpi	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to \exists x \in {Base}_{R} i = RSpan (R) (\{x\})$
46	38 45	r19.29a	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to i \cap RPrime (R) \neq \emptyset$
47	46	ralrimiva	$⊢ φ \to \forall i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\}) i \cap RPrime (R) \neq \emptyset$
48		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
49	48 19 18	isufd	$⊢ R \in UFD \leftrightarrow (R \in IDomn \land \forall i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\}) i \cap RPrime (R) \neq \emptyset)$
50	4 47 49	sylanbrc	$⊢ φ \to R \in UFD$

Metamath Proof Explorer

Theorem pidufd

Proof