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 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) (Revised by Thierry Arnoux, 9-May-2025)

	Ref	Expression
Assertion	df-ufd	⊢ UFD = { 𝑟 ∈ CRing ∣ ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( 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		c0g	⊢ 0g
12	4 11	cfv	⊢ ( 0g ‘ 𝑟 )
13	12	csn	⊢ { ( 0g ‘ 𝑟 ) }
14	13	csn	⊢ { { ( 0g ‘ 𝑟 ) } }
15	10 14	cdif	⊢ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } )
16	8	cv	⊢ 𝑖
17		crpm	⊢ RPrime
18	4 17	cfv	⊢ ( RPrime ‘ 𝑟 )
19	16 18	cin	⊢ ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) )
20	19 6	wne	⊢ ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅
21	20 8 15	wral	⊢ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅
22	7 21	wa	⊢ ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ )
23	22 1 2	crab	⊢ { 𝑟 ∈ CRing ∣ ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ ) }
24	0 23	wceq	⊢ UFD = { 𝑟 ∈ CRing ∣ ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑟 ) ∖ { { ( 0g ‘ 𝑟 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ ) }