Theorem isufd2

Description: Alternate definition of unique factorization domains, using integral domains, for nonzero rings. (Contributed by Thierry Arnoux, 18-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		isufd2.1	|- I = ( PrmIdeal ` R )
2		isufd2.2	|- P = ( RPrime ` R )
3		isufd2.3	|- .0. = ( 0g ` R )
4		eqid	|- ( AbsVal ` R ) = ( AbsVal ` R )
5	4 1 2 3	isufd	|- ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) )
6		isidom	|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
7	4	abvn0b	|- ( R e. Domn <-> ( R e. NzRing /\ ( AbsVal ` R ) =/= (/) ) )
8	7	baib	|- ( R e. NzRing -> ( R e. Domn <-> ( AbsVal ` R ) =/= (/) ) )
9	8	anbi2d	|- ( R e. NzRing -> ( ( R e. CRing /\ R e. Domn ) <-> ( R e. CRing /\ ( AbsVal ` R ) =/= (/) ) ) )
10	6 9	bitrid	|- ( R e. NzRing -> ( R e. IDomn <-> ( R e. CRing /\ ( AbsVal ` R ) =/= (/) ) ) )
11	10	anbi1d	|- ( R e. NzRing -> ( ( R e. IDomn /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) <-> ( ( R e. CRing /\ ( AbsVal ` R ) =/= (/) ) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) )
12		anass	|- ( ( ( R e. CRing /\ ( AbsVal ` R ) =/= (/) ) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) )
13	11 12	bitr2di	|- ( R e. NzRing -> ( ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) <-> ( R e. IDomn /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) )
14	5 13	bitrid	|- ( R e. NzRing -> ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) )