dfufd2

Description: Alternative definition of unique factorization domain (UFD). This is often the textbook definition. Chapter VII, Paragraph 3, Section 3, Proposition 2 of BourbakiCAlg2, p. 228. (Contributed by Thierry Arnoux, 6-Jun-2025)

	Ref	Expression
Hypotheses	dfufd2.b	$⊢ B = {Base}_{R}$
	dfufd2.0	$⊢ \underset{˙}{0} = 0_{R}$
	dfufd2.u	$⊢ U = Unit (R)$
	dfufd2.p	$⊢ P = RPrime (R)$
	dfufd2.m	$⊢ M = {mulGrp}_{R}$
Assertion	dfufd2	$⊢ R \in UFD \leftrightarrow (R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f)$

Proof

Step	Hyp	Ref	Expression
1		dfufd2.b	$⊢ B = {Base}_{R}$
2		dfufd2.0	$⊢ \underset{˙}{0} = 0_{R}$
3		dfufd2.u	$⊢ U = Unit (R)$
4		dfufd2.p	$⊢ P = RPrime (R)$
5		dfufd2.m	$⊢ M = {mulGrp}_{R}$
6		id	$⊢ R \in UFD \to R \in UFD$
7	6	ufdidom	$⊢ R \in UFD \to R \in IDomn$
8		simpl	$⊢ (R \in UFD \land x \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to R \in UFD$
9		simpr	$⊢ (R \in UFD \land x \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to x \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
10	9	eldifad	$⊢ (R \in UFD \land x \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to x \in (B ∖ U)$
11	10	eldifad	$⊢ (R \in UFD \land x \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to x \in B$
12	10	eldifbd	$⊢ (R \in UFD \land x \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to \neg x \in U$
13		eldifsni	$⊢ x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \to x \neq \underset{˙}{0}$
14	13	adantl	$⊢ (R \in UFD \land x \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to x \neq \underset{˙}{0}$
15	1 2 3 4 5 8 11 12 14	1arithufd	$⊢ (R \in UFD \land x \in ((B ∖ U) ∖ \{\underset{˙}{0}\})) \to \exists f \in Word P x = \sum_{M} f$
16	15	ralrimiva	$⊢ R \in UFD \to \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f$
17	7 16	jca	$⊢ R \in UFD \to (R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f)$
18		simpl	$⊢ (R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \to R \in IDomn$
19		id	$⊢ R \in IDomn \to R \in IDomn$
20	19	idomringd	$⊢ R \in IDomn \to R \in Ring$
21	20	ad2antrr	$⊢ ((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to R \in Ring$
22		simpr	$⊢ ((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})$
23	22	eldifad	$⊢ ((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \in PrmIdeal (R)$
24		prmidlidl	$⊢ (R \in Ring \land i \in PrmIdeal (R)) \to i \in LIdeal (R)$
25	21 23 24	syl2anc	$⊢ ((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \in LIdeal (R)$
26		eqid	$⊢ LIdeal (R) = LIdeal (R)$
27	1 26	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq B$
28	25 27	syl	$⊢ ((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \subseteq B$
29	28	sselda	$⊢ (((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \to y \in B$
30		simpr	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land y \in U) \to y \in U$
31		simplr	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land y \in U) \to y \in i$
32	21	ad2antrr	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land y \in U) \to R \in Ring$
33	25	ad2antrr	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land y \in U) \to i \in LIdeal (R)$
34	1 3 30 31 32 33	lidlunitel	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land y \in U) \to i = B$
35		eqid	$⊢ \cdot_{R} = \cdot_{R}$
36	1 35	prmidlnr	$⊢ (R \in Ring \land i \in PrmIdeal (R)) \to i \neq B$
37	21 23 36	syl2anc	$⊢ ((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \neq B$
38	37	ad2antrr	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land y \in U) \to i \neq B$
39	38	neneqd	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land y \in U) \to \neg i = B$
40	34 39	pm2.65da	$⊢ (((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \to \neg y \in U$
41	29 40	eldifd	$⊢ (((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \to y \in (B ∖ U)$
42		simpllr	$⊢ (((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \to y \neq \underset{˙}{0}$
43	41 42	eldifsnd	$⊢ (((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \to y \in ((B ∖ U) ∖ \{\underset{˙}{0}\})$
44		eqeq1	$⊢ x = y \to (x = \sum_{M} f \leftrightarrow y = \sum_{M} f)$
45	44	rexbidv	$⊢ x = y \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P y = \sum_{M} f)$
46	45	adantl	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land x = y) \to (\exists f \in Word P x = \sum_{M} f \leftrightarrow \exists f \in Word P y = \sum_{M} f)$
47	43 46	rspcdv	$⊢ (((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \to (\forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f \to \exists f \in Word P y = \sum_{M} f)$
48		simp-5l	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to R \in IDomn$
49	23	ad3antrrr	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to i \in PrmIdeal (R)$
50		simplr	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to f \in Word P$
51		simpr	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to y = \sum_{M} f$
52		simpllr	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to y \in i$
53	51 52	eqeltrrd	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to \sum_{M} f \in i$
54	42	ad2antrr	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to y \neq \underset{˙}{0}$
55	51 54	eqnetrrd	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to \sum_{M} f \neq \underset{˙}{0}$
56	1 2 3 4 5 48 49 50 53 55	dfufd2lem	$⊢ (((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land f \in Word P) \land y = \sum_{M} f) \to i \cap P \neq \emptyset$
57	56	rexlimdva2	$⊢ (((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \to (\exists f \in Word P y = \sum_{M} f \to i \cap P \neq \emptyset)$
58	47 57	syld	$⊢ (((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \to (\forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f \to i \cap P \neq \emptyset)$
59	58	imp	$⊢ ((((R \in IDomn \land y \neq \underset{˙}{0}) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \to i \cap P \neq \emptyset$
60	59	an52ds	$⊢ ((((R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \land y \in i) \land y \neq \underset{˙}{0}) \to i \cap P \neq \emptyset$
61	20	ad2antrr	$⊢ ((R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to R \in Ring$
62		simpr	$⊢ ((R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})$
63	62	eldifad	$⊢ ((R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \in PrmIdeal (R)$
64	61 63 24	syl2anc	$⊢ ((R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \in LIdeal (R)$
65		eldifsni	$⊢ i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\}) \to i \neq \{\underset{˙}{0}\}$
66	65	adantl	$⊢ ((R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \neq \{\underset{˙}{0}\}$
67	26 2	lidlnz	$⊢ (R \in Ring \land i \in LIdeal (R) \land i \neq \{\underset{˙}{0}\}) \to \exists y \in i y \neq \underset{˙}{0}$
68	61 64 66 67	syl3anc	$⊢ ((R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to \exists y \in i y \neq \underset{˙}{0}$
69	60 68	r19.29a	$⊢ ((R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \land i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\})) \to i \cap P \neq \emptyset$
70	69	ralrimiva	$⊢ (R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \to \forall i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\}) i \cap P \neq \emptyset$
71		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
72	71 4 2	isufd	$⊢ R \in UFD \leftrightarrow (R \in IDomn \land \forall i \in (PrmIdeal (R) ∖ \{\{\underset{˙}{0}\}\}) i \cap P \neq \emptyset)$
73	18 70 72	sylanbrc	$⊢ (R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f) \to R \in UFD$
74	17 73	impbii	$⊢ R \in UFD \leftrightarrow (R \in IDomn \land \forall x \in ((B ∖ U) ∖ \{\underset{˙}{0}\}) \exists f \in Word P x = \sum_{M} f)$

Metamath Proof Explorer

Theorem dfufd2

Proof