Theorem dfufd2 33483

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.)

Hypotheses

Ref	Expression
dfufd2.b	⊢ 𝐵 = (Base‘𝑅)
dfufd2.0	⊢ 0 = (0g‘𝑅)
dfufd2.u	⊢ 𝑈 = (Unit‘𝑅)
dfufd2.p	⊢ 𝑃 = (RPrime‘𝑅)
dfufd2.m	⊢ 𝑀 = (mulGrp‘𝑅)

Assertion

Ref	Expression
dfufd2	⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)))

Distinct variable groups:   0 ,𝑓,𝑥   𝐵,𝑓,𝑥   𝑓,𝑀,𝑥   𝑃,𝑓,𝑥   𝑅,𝑓,𝑥   𝑈,𝑓,𝑥

Proof of Theorem dfufd2

Dummy variables 𝑖 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . . 4 ⊢ (𝑅 ∈ UFD → 𝑅 ∈ UFD)
2	1	ufdidom 33475	. . 3 ⊢ (𝑅 ∈ UFD → 𝑅 ∈ IDomn)
3		dfufd2.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑅)
4		dfufd2.0	. . . . 5 ⊢ 0 = (0g‘𝑅)
5		dfufd2.u	. . . . 5 ⊢ 𝑈 = (Unit‘𝑅)
6		dfufd2.p	. . . . 5 ⊢ 𝑃 = (RPrime‘𝑅)
7		dfufd2.m	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
8		simpl 482	. . . . 5 ⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑅 ∈ UFD)
9		simpr 484	. . . . . . 7 ⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
10	9	eldifad 3911	. . . . . 6 ⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ 𝑈))
11	10	eldifad 3911	. . . . 5 ⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ∈ 𝐵)
12	10	eldifbd 3912	. . . . 5 ⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → ¬ 𝑥 ∈ 𝑈)
13		eldifsni 4739	. . . . . 6 ⊢ (𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }) → 𝑥 ≠ 0 )
14	13	adantl 481	. . . . 5 ⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ≠ 0 )
15	3, 4, 5, 6, 7, 8, 11, 12, 14	1arithufd 33481	. . . 4 ⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓))
16	15	ralrimiva 3121	. . 3 ⊢ (𝑅 ∈ UFD → ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓))
17	2, 16	jca 511	. 2 ⊢ (𝑅 ∈ UFD → (𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)))
18		simpl 482	. . 3 ⊢ ((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → 𝑅 ∈ IDomn)
19		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ IDomn → 𝑅 ∈ IDomn)
20	19	idomringd 20597	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Ring)
21	20	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑅 ∈ Ring)
22		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }}))
23	22	eldifad 3911	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (PrmIdeal‘𝑅))
24		prmidlidl 33377	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) → 𝑖 ∈ (LIdeal‘𝑅))
25	21, 23, 24	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (LIdeal‘𝑅))
26		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
27	3, 26	lidlss 21103	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵)
28	25, 27	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ⊆ 𝐵)
29	28	sselda 3931	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ 𝐵)
30		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑦 ∈ 𝑈)
31		simplr 768	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑦 ∈ 𝑖)
32	21	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑅 ∈ Ring)
33	25	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑖 ∈ (LIdeal‘𝑅))
34	3, 5, 30, 31, 32, 33	lidlunitel 33356	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑖 = 𝐵)
35		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (.r‘𝑅) = (.r‘𝑅)
36	3, 35	prmidlnr 33372	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) → 𝑖 ≠ 𝐵)
37	21, 23, 36	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ≠ 𝐵)
38	37	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑖 ≠ 𝐵)
39	38	neneqd 2930	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → ¬ 𝑖 = 𝐵)
40	34, 39	pm2.65da 816	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → ¬ 𝑦 ∈ 𝑈)
41	29, 40	eldifd 3910	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ (𝐵 ∖ 𝑈))
42		simpllr 775	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ≠ 0 )
43	41, 42	eldifsnd 4736	. . . . . . . . 9 ⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }))
44		eqeq1 2733	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑀 Σg 𝑓) ↔ 𝑦 = (𝑀 Σg 𝑓)))
45	44	rexbidv 3153	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓)))
46	45	adantl 481	. . . . . . . . 9 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑥 = 𝑦) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓)))
47	43, 46	rspcdv 3566	. . . . . . . 8 ⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → (∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) → ∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓)))
48		simp-5l 784	. . . . . . . . . 10 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑅 ∈ IDomn)
49	23	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑖 ∈ (PrmIdeal‘𝑅))
50		simplr 768	. . . . . . . . . 10 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑓 ∈ Word 𝑃)
51		simpr 484	. . . . . . . . . . 11 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑦 = (𝑀 Σg 𝑓))
52		simpllr 775	. . . . . . . . . . 11 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑦 ∈ 𝑖)
53	51, 52	eqeltrrd 2829	. . . . . . . . . 10 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑀 Σg 𝑓) ∈ 𝑖)
54	42	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑦 ≠ 0 )
55	51, 54	eqnetrrd 2993	. . . . . . . . . 10 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑀 Σg 𝑓) ≠ 0 )
56	3, 4, 5, 6, 7, 48, 49, 50, 53, 55	dfufd2lem 33482	. . . . . . . . 9 ⊢ ((((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑖 ∩ 𝑃) ≠ ∅)
57	56	rexlimdva2 3132	. . . . . . . 8 ⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → (∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓) → (𝑖 ∩ 𝑃) ≠ ∅))
58	47, 57	syld 47	. . . . . . 7 ⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → (∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) → (𝑖 ∩ 𝑃) ≠ ∅))
59	58	imp 406	. . . . . 6 ⊢ (((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → (𝑖 ∩ 𝑃) ≠ ∅)
60	59	an52ds 32382	. . . . 5 ⊢ (((((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ≠ 0 ) → (𝑖 ∩ 𝑃) ≠ ∅)
61	20	ad2antrr 726	. . . . . 6 ⊢ (((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑅 ∈ Ring)
62		simpr 484	. . . . . . . 8 ⊢ (((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }}))
63	62	eldifad 3911	. . . . . . 7 ⊢ (((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (PrmIdeal‘𝑅))
64	61, 63, 24	syl2anc 584	. . . . . 6 ⊢ (((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (LIdeal‘𝑅))
65		eldifsni 4739	. . . . . . 7 ⊢ (𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }}) → 𝑖 ≠ { 0 })
66	65	adantl 481	. . . . . 6 ⊢ (((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ≠ { 0 })
67	26, 4	lidlnz 21133	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ { 0 }) → ∃𝑦 ∈ 𝑖 𝑦 ≠ 0 )
68	61, 64, 66, 67	syl3anc 1373	. . . . 5 ⊢ (((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → ∃𝑦 ∈ 𝑖 𝑦 ≠ 0 )
69	60, 68	r19.29a 3137	. . . 4 ⊢ (((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → (𝑖 ∩ 𝑃) ≠ ∅)
70	69	ralrimiva 3121	. . 3 ⊢ ((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → ∀𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅)
71		eqid 2729	. . . 4 ⊢ (PrmIdeal‘𝑅) = (PrmIdeal‘𝑅)
72	71, 6, 4	isufd 33473	. . 3 ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅))
73	18, 70, 72	sylanbrc 583	. 2 ⊢ ((𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → 𝑅 ∈ UFD)
74	17, 73	impbii 209	1 ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  ∅c0 4280  {csn 4573  ‘cfv 6476  (class class class)co 7340  Word cword 14408  Basecbs 17107  ._rcmulr 17149  0_gc0g 17330   Σ_g cgsu 17331  mulGrpcmgp 20012  Ringcrg 20105  Unitcui 20227  RPrimecrpm 20304  IDomncidom 20562  LIdealclidl 21097  PrmIdealcprmidl 33368  UFDcufd 33471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5214  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367  ax-un 7662  ax-ac2 10345  ax-cnex 11053  ax-resscn 11054  ax-1cn 11055  ax-icn 11056  ax-addcl 11057  ax-addrcl 11058  ax-mulcl 11059  ax-mulrcl 11060  ax-mulcom 11061  ax-addass 11062  ax-mulass 11063  ax-distr 11064  ax-i2m1 11065  ax-1ne0 11066  ax-1rid 11067  ax-rnegex 11068  ax-rrecex 11069  ax-cnre 11070  ax-pre-lttri 11071  ax-pre-lttrn 11072  ax-pre-ltadd 11073  ax-pre-mulgt0 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3393  df-v 3435  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-int 4895  df-iun 4940  df-br 5089  df-opab 5151  df-mpt 5170  df-tr 5196  df-id 5508  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5566  df-se 5567  df-we 5568  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-isom 6485  df-riota 7297  df-ov 7343  df-oprab 7344  df-mpo 7345  df-rpss 7650  df-om 7791  df-1st 7915  df-2nd 7916  df-supp 8085  df-tpos 8150  df-frecs 8205  df-wrecs 8236  df-recs 8285  df-rdg 8323  df-1o 8379  df-oadd 8383  df-er 8616  df-en 8864  df-dom 8865  df-sdom 8866  df-fin 8867  df-fsupp 9240  df-oi 9390  df-dju 9785  df-card 9823  df-ac 9998  df-pnf 11139  df-mnf 11140  df-xr 11141  df-ltxr 11142  df-le 11143  df-sub 11337  df-neg 11338  df-nn 12117  df-2 12179  df-3 12180  df-4 12181  df-5 12182  df-6 12183  df-7 12184  df-8 12185  df-n0 12373  df-xnn0 12446  df-z 12460  df-uz 12724  df-fz 13399  df-fzo 13546  df-seq 13897  df-hash 14226  df-word 14409  df-lsw 14458  df-concat 14466  df-s1 14491  df-substr 14536  df-pfx 14566  df-sets 17062  df-slot 17080  df-ndx 17092  df-base 17108  df-ress 17129  df-plusg 17161  df-mulr 17162  df-sca 17164  df-vsca 17165  df-ip 17166  df-0g 17332  df-gsum 17333  df-mgm 18501  df-sgrp 18580  df-mnd 18596  df-submnd 18645  df-grp 18802  df-minusg 18803  df-sbg 18804  df-subg 18989  df-cntz 19183  df-lsm 19502  df-cmn 19648  df-abl 19649  df-mgp 20013  df-rng 20025  df-ur 20054  df-ring 20107  df-cring 20108  df-oppr 20209  df-dvdsr 20229  df-unit 20230  df-invr 20260  df-rprm 20305  df-nzr 20382  df-subrg 20439  df-domn 20564  df-idom 20565  df-drng 20600  df-lmod 20749  df-lss 20819  df-lsp 20859  df-sra 21061  df-rgmod 21062  df-lidl 21099  df-rsp 21100  df-prmidl 33369  df-ufd 33472

This theorem is referenced by: (None)