Metamath Proof Explorer

Definition df-ufd

Description: Define the class of unique factorization domains. A unique factorization domain (UFD for short), is an integral domain such that every nonzero prime ideal contains a prime element (this is a characterization due to Irving Kaplansky). A UFD is sometimes also called a "factorial ring" following the terminology of Bourbaki. (Contributed by Mario Carneiro, 17-Feb-2015) Exclude the 0 prime ideal. (Revised by Thierry Arnoux, 9-May-2025) Exclude the 0 ring. (Revised by Thierry Arnoux, 14-Jun-2025)

Ref Expression
Assertion df-ufd ⊢ UFD = r ∈ IDomn | ∀ i ∈ PrmIdeal ⁡ r ∖ 0 r i ∩ RPrime ⁡ r ≠ ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 cufd class UFD
1 vr setvar r
2 cidom class IDomn
3 vi setvar i
4 cprmidl class PrmIdeal
5 1 cv setvar r
6 5 4 cfv class PrmIdeal ⁡ r
7 c0g class 0 𝑔
8 5 7 cfv class 0 r
9 8 csn class 0 r
10 9 csn class 0 r
11 6 10 cdif class PrmIdeal ⁡ r ∖ 0 r
12 3 cv setvar i
13 crpm class RPrime
14 5 13 cfv class RPrime ⁡ r
15 12 14 cin class i ∩ RPrime ⁡ r
16 c0 class ∅
17 15 16 wne wff i ∩ RPrime ⁡ r ≠ ∅
18 17 3 11 wral wff ∀ i ∈ PrmIdeal ⁡ r ∖ 0 r i ∩ RPrime ⁡ r ≠ ∅
19 18 1 2 crab class r ∈ IDomn | ∀ i ∈ PrmIdeal ⁡ r ∖ 0 r i ∩ RPrime ⁡ r ≠ ∅
20 0 19 wceq wff UFD = r ∈ IDomn | ∀ i ∈ PrmIdeal ⁡ r ∖ 0 r i ∩ RPrime ⁡ r ≠ ∅