Theorem ufdidom

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

	Ref	Expression
Hypothesis	ufdidom.2	⊢ ( 𝜑 → 𝑅 ∈ UFD )
Assertion	ufdidom	⊢ ( 𝜑 → 𝑅 ∈ IDomn )

Proof

Step	Hyp	Ref	Expression
1		ufdidom.2	⊢ ( 𝜑 → 𝑅 ∈ UFD )
2		eqid	⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
3		eqid	⊢ ( RPrime ‘ 𝑅 ) = ( RPrime ‘ 𝑅 )
4		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5	2 3 4	isufd	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ) )
6	5	simplbi	⊢ ( 𝑅 ∈ UFD → 𝑅 ∈ IDomn )
7	1 6	syl	⊢ ( 𝜑 → 𝑅 ∈ IDomn )