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 = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cufd	|- UFD
1		vr	|- r
2		ccrg	|- CRing
3		cabv	|- AbsVal
4	1	cv	|- r
5	4 3	cfv	|- ( AbsVal ` r )
6		c0	|- (/)
7	5 6	wne	|- ( AbsVal ` r ) =/= (/)
8		vi	|- i
9		cprmidl	|- PrmIdeal
10	4 9	cfv	|- ( PrmIdeal ` r )
11		c0g	|- 0g
12	4 11	cfv	|- ( 0g ` r )
13	12	csn	|- { ( 0g ` r ) }
14	13	csn	|- { { ( 0g ` r ) } }
15	10 14	cdif	|- ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } )
16	8	cv	|- i
17		crpm	|- RPrime
18	4 17	cfv	|- ( RPrime ` r )
19	16 18	cin	|- ( i i^i ( RPrime ` r ) )
20	19 6	wne	|- ( i i^i ( RPrime ` r ) ) =/= (/)
21	20 8 15	wral	|- A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/)
22	7 21	wa	|- ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) )
23	22 1 2	crab	|- { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) }
24	0 23	wceq	|- UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) }