Metamath Proof Explorer

Theorem ufdcringd

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

Ref Expression
Hypothesis ufdcringd.1 
|- ( ph -> R e. UFD )
Assertion ufdcringd 
|- ( ph -> R e. CRing )

Proof

Step Hyp Ref Expression
1 ufdcringd.1 
 |-  ( ph -> R e. UFD )
2 eqid 
 |-  ( AbsVal ` R ) = ( AbsVal ` R )
3 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
4 eqid 
 |-  ( RPrime ` R ) = ( RPrime ` R )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 2 3 4 5 isufd 
 |-  ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) )
7 1 6 sylib 
 |-  ( ph -> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) )
8 7 simpld 
 |-  ( ph -> R e. CRing )