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 )
isufd.0 
|- .0. = ( 0g ` R )
Assertion isufd 
|- ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( 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 isufd.0 
 |-  .0. = ( 0g ` R )
5 fveq2 
 |-  ( r = R -> ( AbsVal ` r ) = ( AbsVal ` R ) )
6 5 1 eqtr4di 
 |-  ( r = R -> ( AbsVal ` r ) = A )
7 6 neeq1d 
 |-  ( r = R -> ( ( AbsVal ` r ) =/= (/) <-> A =/= (/) ) )
8 fveq2 
 |-  ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) )
9 8 2 eqtr4di 
 |-  ( r = R -> ( PrmIdeal ` r ) = I )
10 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
11 10 4 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
12 11 sneqd 
 |-  ( r = R -> { ( 0g ` r ) } = { .0. } )
13 12 sneqd 
 |-  ( r = R -> { { ( 0g ` r ) } } = { { .0. } } )
14 9 13 difeq12d 
 |-  ( r = R -> ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) = ( I \ { { .0. } } ) )
15 fveq2 
 |-  ( r = R -> ( RPrime ` r ) = ( RPrime ` R ) )
16 15 3 eqtr4di 
 |-  ( r = R -> ( RPrime ` r ) = P )
17 16 ineq2d 
 |-  ( r = R -> ( i i^i ( RPrime ` r ) ) = ( i i^i P ) )
18 17 neeq1d 
 |-  ( r = R -> ( ( i i^i ( RPrime ` r ) ) =/= (/) <-> ( i i^i P ) =/= (/) ) )
19 14 18 raleqbidv 
 |-  ( r = R -> ( A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) <-> A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) )
20 7 19 anbi12d 
 |-  ( r = R -> ( ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) <-> ( A =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) )
21 df-ufd 
 |-  UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) }
22 20 21 elrab2 
 |-  ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) )