Definition df-ufd

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cufd	⊢ UFD
1		vr	⊢ 𝑟
2		ccrg	⊢ CRing
3		cabv	⊢ AbsVal
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( AbsVal ‘ 𝑟 )
6		c0	⊢ ∅
7	5 6	wne	⊢ ( AbsVal ‘ 𝑟 ) ≠ ∅
8		vi	⊢ 𝑖
9		cprmidl	⊢ PrmIdeal
10	4 9	cfv	⊢ ( PrmIdeal ‘ 𝑟 )
11	8	cv	⊢ 𝑖
12		crpm	⊢ RPrime
13	4 12	cfv	⊢ ( RPrime ‘ 𝑟 )
14	11 13	cin	⊢ ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) )
15	14 6	wne	⊢ ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅
16	15 8 10	wral	⊢ ∀ 𝑖 ∈ ( PrmIdeal ‘ 𝑟 ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅
17	7 16	wa	⊢ ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( PrmIdeal ‘ 𝑟 ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ )
18	17 1 2	crab	⊢ { 𝑟 ∈ CRing ∣ ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( PrmIdeal ‘ 𝑟 ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ ) }
19	0 18	wceq	⊢ UFD = { 𝑟 ∈ CRing ∣ ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( PrmIdeal ‘ 𝑟 ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ ) }