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		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\})$
22		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}$
23	22	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}\}$
24	23	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}\})$
25	9 18	rsp0	$⊢ R \in Ring \to RSpan (R) (\{0_{R}\}) = \{0_{R}\}$
26	5 25	syl	$⊢ φ \to RSpan (R) (\{0_{R}\}) = \{0_{R}\}$
27	26	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}\}$
28	21 24 27	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}\}$
29		eldifsni	$⊢ i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\}) \to i \neq \{0_{R}\}$
30	29	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}\}$
31	30	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}\}$
32	28 31	pm2.65da	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to \neg x = 0_{R}$
33	32	neqned	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to x \neq 0_{R}$
34	18 8 19 9 20 7 33	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))$
35	17 34	mpbird	$⊢ (((φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \land x \in {Base}_{R}) \land i = RSpan (R) (\{x\})) \to x \in RPrime (R)$
36	13 35	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))$
37	36	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$
38		eqid	$⊢ LIdeal (R) = LIdeal (R)$
39	3	elin2d	$⊢ φ \to R \in LPIR$
40	39	adantr	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to R \in LPIR$
41	5	adantr	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to R \in Ring$
42		prmidlidl	$⊢ (R \in Ring \land i \in PrmIdeal (R)) \to i \in LIdeal (R)$
43	41 15 42	syl2anc	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to i \in LIdeal (R)$
44	8 38 9 40 43	lpirlidllpi	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to \exists x \in {Base}_{R} i = RSpan (R) (\{x\})$
45	37 44	r19.29a	$⊢ (φ \land i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\})) \to i \cap RPrime (R) \neq \emptyset$
46	45	ralrimiva	$⊢ φ \to \forall i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\}) i \cap RPrime (R) \neq \emptyset$
47		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
48	47 19 18	isufd	$⊢ R \in UFD \leftrightarrow (R \in IDomn \land \forall i \in (PrmIdeal (R) ∖ \{\{0_{R}\}\}) i \cap RPrime (R) \neq \emptyset)$
49	4 46 48	sylanbrc	$⊢ φ \to R \in UFD$

Metamath Proof Explorer

Theorem pidufd

Proof