Metamath Proof Explorer

Theorem isufd

Description: The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses isufd.a 
|- A = ( AbsVal ` R )
isufd.i 
|- I = ( PrmIdeal ` R )
isufd.3 
|- P = ( RPrime ` R )
Assertion isufd 
|- ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. I ( i i^i P ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 isufd.a 
 |-  A = ( AbsVal ` R )
2 isufd.i 
 |-  I = ( PrmIdeal ` R )
3 isufd.3 
 |-  P = ( RPrime ` R )
4 fveq2 
 |-  ( r = R -> ( AbsVal ` r ) = ( AbsVal ` R ) )
5 4 1 eqtr4di 
 |-  ( r = R -> ( AbsVal ` r ) = A )
6 5 neeq1d 
 |-  ( r = R -> ( ( AbsVal ` r ) =/= (/) <-> A =/= (/) ) )
7 fveq2 
 |-  ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) )
8 7 2 eqtr4di 
 |-  ( r = R -> ( PrmIdeal ` r ) = I )
9 fveq2 
 |-  ( r = R -> ( RPrime ` r ) = ( RPrime ` R ) )
10 9 3 eqtr4di 
 |-  ( r = R -> ( RPrime ` r ) = P )
11 10 ineq2d 
 |-  ( r = R -> ( i i^i ( RPrime ` r ) ) = ( i i^i P ) )
12 11 neeq1d 
 |-  ( r = R -> ( ( i i^i ( RPrime ` r ) ) =/= (/) <-> ( i i^i P ) =/= (/) ) )
13 8 12 raleqbidv 
 |-  ( r = R -> ( A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) <-> A. i e. I ( i i^i P ) =/= (/) ) )
14 6 13 anbi12d 
 |-  ( r = R -> ( ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) ) <-> ( A =/= (/) /\ A. i e. I ( i i^i P ) =/= (/) ) ) )
15 df-ufd 
 |-  UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) ) }
16 14 15 elrab2 
 |-  ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. I ( i i^i P ) =/= (/) ) ) )