Theorem ufdcringd

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

	Ref	Expression
Hypothesis	ufdcringd.1	No typesetting found for |- ( ph -> R e. UFD ) with typecode |-
Assertion	ufdcringd	$$⊢\phi \to R\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		ufdcringd.1	Could not format ( ph -> R e. UFD ) : No typesetting found for |- ( ph -> R e. UFD ) with typecode |-
2		eqid	$$⊢\mathrm{AbsVal}\left(R\right)=\mathrm{AbsVal}\left(R\right)$$
3		eqid	Could not format ( PrmIdeal ` R ) = ( PrmIdeal ` R ) : No typesetting found for |- ( PrmIdeal ` R ) = ( PrmIdeal ` R ) with typecode |-
4		eqid	$$⊢\mathrm{RPrime}\left(R\right)=\mathrm{RPrime}\left(R\right)$$
5		eqid	$$⊢0_R=0_R$$
6	2 3 4 5	isufd	Could not format ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) ) : No typesetting found for |- ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) ) with typecode |-
7	1 6	sylib	Could not format ( ph -> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) ) : No typesetting found for |- ( ph -> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) ) with typecode |-
8	7	simpld	$$⊢\phi \to R\in \mathrm{CRing}$$