Theorem ufdidom

Description: A nonzero unique factorization domain is an integral domain. (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypothesis	ufdidom.2	|- ( ph -> R e. UFD )
Assertion	ufdidom	|- ( ph -> R e. IDomn )

Proof

Step	Hyp	Ref	Expression
1		ufdidom.2	|- ( ph -> R e. UFD )
2		eqid	|- ( PrmIdeal ` R ) = ( PrmIdeal ` R )
3		eqid	|- ( RPrime ` R ) = ( RPrime ` R )
4		eqid	|- ( 0g ` R ) = ( 0g ` R )
5	2 3 4	isufd	|- ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) )
6	5	simplbi	|- ( R e. UFD -> R e. IDomn )
7	1 6	syl	|- ( ph -> R e. IDomn )