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 = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` 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	8	cv	|- i
12		crpm	|- RPrime
13	4 12	cfv	|- ( RPrime ` r )
14	11 13	cin	|- ( i i^i ( RPrime ` r ) )
15	14 6	wne	|- ( i i^i ( RPrime ` r ) ) =/= (/)
16	15 8 10	wral	|- A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/)
17	7 16	wa	|- ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) )
18	17 1 2	crab	|- { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) ) }
19	0 18	wceq	|- UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) ) }