Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dfufd2.0 ⊢ 0 = ( 0g ‘ 𝑅 )
dfufd2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dfufd2.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
dfufd2.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion dfufd2 ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑥 ∈ ( ( 𝐵 ∖ 𝑈 ) ∖ { 0 } ) ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ) )

Proof

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