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 |
|
neeq1 |
|- ( f = F -> ( f =/= .0. <-> F =/= .0. ) ) |
8 |
|
fveq2 |
|- ( f = F -> ( coe1 ` f ) = ( coe1 ` F ) ) |
9 |
|
fveq2 |
|- ( f = F -> ( D ` f ) = ( D ` F ) ) |
10 |
8 9
|
fveq12d |
|- ( f = F -> ( ( coe1 ` f ) ` ( D ` f ) ) = ( ( coe1 ` F ) ` ( D ` F ) ) ) |
11 |
10
|
eleq1d |
|- ( f = F -> ( ( ( coe1 ` f ) ` ( D ` f ) ) e. U <-> ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) |
12 |
7 11
|
anbi12d |
|- ( f = F -> ( ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) <-> ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) ) |
13 |
1 2 3 4 5 6
|
uc1pval |
|- C = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } |
14 |
12 13
|
elrab2 |
|- ( F e. C <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) ) |
15 |
|
3anass |
|- ( ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) ) |
16 |
14 15
|
bitr4i |
|- ( F e. C <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) |