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 e. IDomn | 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		cidom	|- IDomn
3		vi	|- i
4		cprmidl	|- PrmIdeal
5	1	cv	|- r
6	5 4	cfv	|- ( PrmIdeal ` r )
7		c0g	|- 0g
8	5 7	cfv	|- ( 0g ` r )
9	8	csn	|- { ( 0g ` r ) }
10	9	csn	|- { { ( 0g ` r ) } }
11	6 10	cdif	|- ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } )
12	3	cv	|- i
13		crpm	|- RPrime
14	5 13	cfv	|- ( RPrime ` r )
15	12 14	cin	|- ( i i^i ( RPrime ` r ) )
16		c0	|- (/)
17	15 16	wne	|- ( i i^i ( RPrime ` r ) ) =/= (/)
18	17 3 11	wral	|- A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/)
19	18 1 2	crab	|- { r e. IDomn | A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) }
20	0 19	wceq	|- UFD = { r e. IDomn | A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) }