Step |
Hyp |
Ref |
Expression |
1 |
|
deg1z.d |
|- D = ( deg1 ` R ) |
2 |
|
deg1z.p |
|- P = ( Poly1 ` R ) |
3 |
|
deg1z.z |
|- .0. = ( 0g ` P ) |
4 |
|
deg1nn0cl.b |
|- B = ( Base ` P ) |
5 |
|
deg1ldg.y |
|- Y = ( 0g ` R ) |
6 |
|
deg1ldg.a |
|- A = ( coe1 ` F ) |
7 |
1
|
deg1fval |
|- D = ( 1o mDeg R ) |
8 |
|
eqid |
|- ( 1o mPoly R ) = ( 1o mPoly R ) |
9 |
|
eqid |
|- ( PwSer1 ` R ) = ( PwSer1 ` R ) |
10 |
2 9 4
|
ply1bas |
|- B = ( Base ` ( 1o mPoly R ) ) |
11 |
|
psr1baslem |
|- ( NN0 ^m 1o ) = { c e. ( NN0 ^m 1o ) | ( `' c " NN ) e. Fin } |
12 |
|
tdeglem2 |
|- ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( CCfld gsum a ) ) |
13 |
8 2 3
|
ply1mpl0 |
|- .0. = ( 0g ` ( 1o mPoly R ) ) |
14 |
7 8 10 5 11 12 13
|
mdegldg |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> E. b e. ( NN0 ^m 1o ) ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) ) |
15 |
6
|
fvcoe1 |
|- ( ( F e. B /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( b ` (/) ) ) ) |
16 |
15
|
3ad2antl2 |
|- ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( b ` (/) ) ) ) |
17 |
|
fveq1 |
|- ( a = b -> ( a ` (/) ) = ( b ` (/) ) ) |
18 |
|
eqid |
|- ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) |
19 |
|
fvex |
|- ( b ` (/) ) e. _V |
20 |
17 18 19
|
fvmpt |
|- ( b e. ( NN0 ^m 1o ) -> ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( b ` (/) ) ) |
21 |
20
|
fveq2d |
|- ( b e. ( NN0 ^m 1o ) -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` ( b ` (/) ) ) ) |
22 |
21
|
adantl |
|- ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` ( b ` (/) ) ) ) |
23 |
16 22
|
eqtr4d |
|- ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) ) |
24 |
23
|
neeq1d |
|- ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( ( F ` b ) =/= Y <-> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) ) |
25 |
24
|
anbi1d |
|- ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> ( ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) ) ) |
26 |
25
|
biancomd |
|- ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) ) ) |
27 |
26
|
rexbidva |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. b e. ( NN0 ^m 1o ) ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> E. b e. ( NN0 ^m 1o ) ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) ) ) |
28 |
|
df1o2 |
|- 1o = { (/) } |
29 |
|
nn0ex |
|- NN0 e. _V |
30 |
|
0ex |
|- (/) e. _V |
31 |
28 29 30 18
|
mapsnf1o2 |
|- ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 |
32 |
|
f1ofo |
|- ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 -> ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0 ) |
33 |
|
eqeq1 |
|- ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) <-> d = ( D ` F ) ) ) |
34 |
|
fveq2 |
|- ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` d ) ) |
35 |
34
|
neeq1d |
|- ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y <-> ( A ` d ) =/= Y ) ) |
36 |
33 35
|
anbi12d |
|- ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) <-> ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) ) ) |
37 |
36
|
cbvexfo |
|- ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0 -> ( E. b e. ( NN0 ^m 1o ) ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) <-> E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) ) ) |
38 |
31 32 37
|
mp2b |
|- ( E. b e. ( NN0 ^m 1o ) ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) <-> E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) ) |
39 |
27 38
|
bitrdi |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. b e. ( NN0 ^m 1o ) ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) ) ) |
40 |
1 2 3 4
|
deg1nn0cl |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 ) |
41 |
|
fveq2 |
|- ( d = ( D ` F ) -> ( A ` d ) = ( A ` ( D ` F ) ) ) |
42 |
41
|
neeq1d |
|- ( d = ( D ` F ) -> ( ( A ` d ) =/= Y <-> ( A ` ( D ` F ) ) =/= Y ) ) |
43 |
42
|
ceqsrexv |
|- ( ( D ` F ) e. NN0 -> ( E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) <-> ( A ` ( D ` F ) ) =/= Y ) ) |
44 |
40 43
|
syl |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) <-> ( A ` ( D ` F ) ) =/= Y ) ) |
45 |
39 44
|
bitrd |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. b e. ( NN0 ^m 1o ) ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> ( A ` ( D ` F ) ) =/= Y ) ) |
46 |
14 45
|
mpbid |
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= Y ) |