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 ) =/= (/) ) ) ) |