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	Could not format assertion : No typesetting found for |- UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cufd	Could not format UFD : No typesetting found for class UFD with typecode class
1		vr	$$setvarr$$
2		ccrg	$$class\mathrm{CRing}$$
3		cabv	$$class\mathrm{AbsVal}$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class\mathrm{AbsVal}\left(r\right)$$
6		c0	$$class\varnothing$$
7	5 6	wne	$$wff\mathrm{AbsVal}\left(r\right)\ne \varnothing$$
8		vi	$$setvari$$
9		cprmidl	Could not format PrmIdeal : No typesetting found for class PrmIdeal with typecode class
10	4 9	cfv	Could not format ( PrmIdeal ` r ) : No typesetting found for class ( PrmIdeal ` r ) with typecode class
11		c0g	$$class{0}_{𝑔}$$
12	4 11	cfv	$$class{0}_r$$
13	12	csn	$$class\left\{0_r\right\}$$
14	13	csn	$$class\left\{\left\{0_r\right\}\right\}$$
15	10 14	cdif	Could not format ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) : No typesetting found for class ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) with typecode class
16	8	cv	$$setvari$$
17		crpm	$$class\mathrm{RPrime}$$
18	4 17	cfv	$$class\mathrm{RPrime}\left(r\right)$$
19	16 18	cin	$$class\left(i\cap \mathrm{RPrime}\left(r\right)\right)$$
20	19 6	wne	$$wffi\cap \mathrm{RPrime}\left(r\right)\ne \varnothing$$
21	20 8 15	wral	Could not format A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) : No typesetting found for wff A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) with typecode wff
22	7 21	wa	Could not format ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) : No typesetting found for wff ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) with typecode wff
23	22 1 2	crab	Could not format { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } : No typesetting found for class { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } with typecode class
24	0 23	wceq	Could not format UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } : No typesetting found for wff UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } with typecode wff