Definition df-ufd 31187

Description: Define the class of unique factorization domains. A unique factorization domain (UFD for short), is a commutative ring with an absolute value (from abvtriv 19685 this is equivalent to being a domain) such that every 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.)

Assertion

Ref	Expression
df-ufd	⊢ UFD = {𝑟 ∈ CRing ∣ ((AbsVal‘𝑟) ≠ ∅ ∧ ∀𝑖 ∈ (PrmIdeal‘𝑟)(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅)}

Distinct variable group:   𝑖,𝑟

Detailed syntax breakdown of Definition df-ufd

Step	Hyp	Ref	Expression
1		cufd 31186	. 2 class UFD
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1537	. . . . . 6 class 𝑟
4		cabv 19660	. . . . . 6 class AbsVal
5	3, 4	cfv 6339	. . . . 5 class (AbsVal‘𝑟)
6		c0 4227	. . . . 5 class ∅
7	5, 6	wne 2951	. . . 4 wff (AbsVal‘𝑟) ≠ ∅
8		vi	. . . . . . . 8 setvar 𝑖
9	8	cv 1537	. . . . . . 7 class 𝑖
10		crpm 19538	. . . . . . . 8 class RPrime
11	3, 10	cfv 6339	. . . . . . 7 class (RPrime‘𝑟)
12	9, 11	cin 3859	. . . . . 6 class (𝑖 ∩ (RPrime‘𝑟))
13	12, 6	wne 2951	. . . . 5 wff (𝑖 ∩ (RPrime‘𝑟)) ≠ ∅
14		cprmidl 31135	. . . . . 6 class PrmIdeal
15	3, 14	cfv 6339	. . . . 5 class (PrmIdeal‘𝑟)
16	13, 8, 15	wral 3070	. . . 4 wff ∀𝑖 ∈ (PrmIdeal‘𝑟)(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅
17	7, 16	wa 399	. . 3 wff ((AbsVal‘𝑟) ≠ ∅ ∧ ∀𝑖 ∈ (PrmIdeal‘𝑟)(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅)
18		ccrg 19371	. . 3 class CRing
19	17, 2, 18	crab 3074	. 2 class {𝑟 ∈ CRing ∣ ((AbsVal‘𝑟) ≠ ∅ ∧ ∀𝑖 ∈ (PrmIdeal‘𝑟)(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅)}
20	1, 19	wceq 1538	1 wff UFD = {𝑟 ∈ CRing ∣ ((AbsVal‘𝑟) ≠ ∅ ∧ ∀𝑖 ∈ (PrmIdeal‘𝑟)(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅)}

This definition is referenced by:  isufd  31188