Theorem ufdcringd

Description: A unique factorization domain is a commutative ring. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypothesis	ufdcringd.1	⊢ ( 𝜑 → 𝑅 ∈ UFD )
Assertion	ufdcringd	⊢ ( 𝜑 → 𝑅 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		ufdcringd.1	⊢ ( 𝜑 → 𝑅 ∈ UFD )
2		eqid	⊢ ( AbsVal ‘ 𝑅 ) = ( AbsVal ‘ 𝑅 )
3		eqid	⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
4		eqid	⊢ ( RPrime ‘ 𝑅 ) = ( RPrime ‘ 𝑅 )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6	2 3 4 5	isufd	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ CRing ∧ ( ( AbsVal ‘ 𝑅 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ) ) )
7	1 6	sylib	⊢ ( 𝜑 → ( 𝑅 ∈ CRing ∧ ( ( AbsVal ‘ 𝑅 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ) ) )
8	7	simpld	⊢ ( 𝜑 → 𝑅 ∈ CRing )