Step |
Hyp |
Ref |
Expression |
1 |
|
uc1pval.p |
|- P = ( Poly1 ` R ) |
2 |
|
uc1pval.b |
|- B = ( Base ` P ) |
3 |
|
uc1pval.z |
|- .0. = ( 0g ` P ) |
4 |
|
uc1pval.d |
|- D = ( deg1 ` R ) |
5 |
|
uc1pval.c |
|- C = ( Unic1p ` R ) |
6 |
|
uc1pval.u |
|- U = ( Unit ` R ) |
7 |
|
fveq2 |
|- ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) ) |
8 |
7 1
|
eqtr4di |
|- ( r = R -> ( Poly1 ` r ) = P ) |
9 |
8
|
fveq2d |
|- ( r = R -> ( Base ` ( Poly1 ` r ) ) = ( Base ` P ) ) |
10 |
9 2
|
eqtr4di |
|- ( r = R -> ( Base ` ( Poly1 ` r ) ) = B ) |
11 |
8
|
fveq2d |
|- ( r = R -> ( 0g ` ( Poly1 ` r ) ) = ( 0g ` P ) ) |
12 |
11 3
|
eqtr4di |
|- ( r = R -> ( 0g ` ( Poly1 ` r ) ) = .0. ) |
13 |
12
|
neeq2d |
|- ( r = R -> ( f =/= ( 0g ` ( Poly1 ` r ) ) <-> f =/= .0. ) ) |
14 |
|
fveq2 |
|- ( r = R -> ( deg1 ` r ) = ( deg1 ` R ) ) |
15 |
14 4
|
eqtr4di |
|- ( r = R -> ( deg1 ` r ) = D ) |
16 |
15
|
fveq1d |
|- ( r = R -> ( ( deg1 ` r ) ` f ) = ( D ` f ) ) |
17 |
16
|
fveq2d |
|- ( r = R -> ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( ( coe1 ` f ) ` ( D ` f ) ) ) |
18 |
|
fveq2 |
|- ( r = R -> ( Unit ` r ) = ( Unit ` R ) ) |
19 |
18 6
|
eqtr4di |
|- ( r = R -> ( Unit ` r ) = U ) |
20 |
17 19
|
eleq12d |
|- ( r = R -> ( ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) <-> ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) ) |
21 |
13 20
|
anbi12d |
|- ( r = R -> ( ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) <-> ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) ) ) |
22 |
10 21
|
rabeqbidv |
|- ( r = R -> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) } = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } ) |
23 |
|
df-uc1p |
|- Unic1p = ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) } ) |
24 |
2
|
fvexi |
|- B e. _V |
25 |
24
|
rabex |
|- { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } e. _V |
26 |
22 23 25
|
fvmpt |
|- ( R e. _V -> ( Unic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } ) |
27 |
|
fvprc |
|- ( -. R e. _V -> ( Unic1p ` R ) = (/) ) |
28 |
|
ssrab2 |
|- { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } C_ B |
29 |
|
fvprc |
|- ( -. R e. _V -> ( Poly1 ` R ) = (/) ) |
30 |
1 29
|
syl5eq |
|- ( -. R e. _V -> P = (/) ) |
31 |
30
|
fveq2d |
|- ( -. R e. _V -> ( Base ` P ) = ( Base ` (/) ) ) |
32 |
|
base0 |
|- (/) = ( Base ` (/) ) |
33 |
31 32
|
eqtr4di |
|- ( -. R e. _V -> ( Base ` P ) = (/) ) |
34 |
2 33
|
syl5eq |
|- ( -. R e. _V -> B = (/) ) |
35 |
28 34
|
sseqtrid |
|- ( -. R e. _V -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } C_ (/) ) |
36 |
|
ss0 |
|- ( { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } C_ (/) -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } = (/) ) |
37 |
35 36
|
syl |
|- ( -. R e. _V -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } = (/) ) |
38 |
27 37
|
eqtr4d |
|- ( -. R e. _V -> ( Unic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } ) |
39 |
26 38
|
pm2.61i |
|- ( Unic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } |
40 |
5 39
|
eqtri |
|- C = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } |