Theorem isufd

Description: The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	isufd.i	|- I = ( PrmIdeal ` R )
	isufd.3	|- P = ( RPrime ` R )
	isufd.0	|- .0. = ( 0g ` R )
Assertion	isufd	|- ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) )

Proof

Step	Hyp	Ref	Expression
1		isufd.i	|- I = ( PrmIdeal ` R )
2		isufd.3	|- P = ( RPrime ` R )
3		isufd.0	|- .0. = ( 0g ` R )
4		fveq2	|- ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) )
5	4 1	eqtr4di	|- ( r = R -> ( PrmIdeal ` r ) = I )
6		fveq2	|- ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
7	6 3	eqtr4di	|- ( r = R -> ( 0g ` r ) = .0. )
8	7	sneqd	|- ( r = R -> { ( 0g ` r ) } = { .0. } )
9	8	sneqd	|- ( r = R -> { { ( 0g ` r ) } } = { { .0. } } )
10	5 9	difeq12d	|- ( r = R -> ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) = ( I \ { { .0. } } ) )
11		fveq2	|- ( r = R -> ( RPrime ` r ) = ( RPrime ` R ) )
12	11 2	eqtr4di	|- ( r = R -> ( RPrime ` r ) = P )
13	12	ineq2d	|- ( r = R -> ( i i^i ( RPrime ` r ) ) = ( i i^i P ) )
14	13	neeq1d	|- ( r = R -> ( ( i i^i ( RPrime ` r ) ) =/= (/) <-> ( i i^i P ) =/= (/) ) )
15	10 14	raleqbidv	|- ( r = R -> ( A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) <-> A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) )
16		df-ufd	|- UFD = { r e. IDomn | A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) }
17	15 16	elrab2	|- ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) )