Metamath Proof Explorer

Theorem deg1leb

Description: Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1leb.d 
|- D = ( deg1 ` R )
deg1leb.p 
|- P = ( Poly1 ` R )
deg1leb.b 
|- B = ( Base ` P )
deg1leb.y 
|- .0. = ( 0g ` R )
deg1leb.a 
|- A = ( coe1 ` F )
Assertion deg1leb 
|- ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> A. x e. NN0 ( G < x -> ( A ` x ) = .0. ) ) )

Proof

Step Hyp Ref Expression
1 deg1leb.d 
 |-  D = ( deg1 ` R )
2 deg1leb.p 
 |-  P = ( Poly1 ` R )
3 deg1leb.b 
 |-  B = ( Base ` P )
4 deg1leb.y 
 |-  .0. = ( 0g ` R )
5 deg1leb.a 
 |-  A = ( coe1 ` F )
6 1 deg1fval 
 |-  D = ( 1o mDeg R )
7 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
8 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
9 2 8 3 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
10 psr1baslem 
 |-  ( NN0 ^m 1o ) = { a e. ( NN0 ^m 1o ) | ( `' a " NN ) e. Fin }
11 tdeglem2 
 |-  ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) = ( b e. ( NN0 ^m 1o ) |-> ( CCfld gsum b ) )
12 6 7 9 4 10 11 mdegleb 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> A. y e. ( NN0 ^m 1o ) ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( F ` y ) = .0. ) ) )
13 df1o2 
 |-  1o = { (/) }
14 nn0ex 
 |-  NN0 e. _V
15 0ex 
 |-  (/) e. _V
16 eqid 
 |-  ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) = ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) )
17 13 14 15 16 mapsnf1o2 
 |-  ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0
18 f1ofo 
 |-  ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 -> ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0 )
19 breq2 
 |-  ( ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) = x -> ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) <-> G < x ) )
20 fveqeq2 
 |-  ( ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) = x -> ( ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = .0. <-> ( A ` x ) = .0. ) )
21 19 20 imbi12d 
 |-  ( ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) = x -> ( ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = .0. ) <-> ( G < x -> ( A ` x ) = .0. ) ) )
22 21 cbvfo 
 |-  ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0 -> ( A. y e. ( NN0 ^m 1o ) ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = .0. ) <-> A. x e. NN0 ( G < x -> ( A ` x ) = .0. ) ) )
23 17 18 22 mp2b 
 |-  ( A. y e. ( NN0 ^m 1o ) ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = .0. ) <-> A. x e. NN0 ( G < x -> ( A ` x ) = .0. ) )
24 fveq1 
 |-  ( b = y -> ( b ` (/) ) = ( y ` (/) ) )
25 fvex 
 |-  ( y ` (/) ) e. _V
26 24 16 25 fvmpt 
 |-  ( y e. ( NN0 ^m 1o ) -> ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) = ( y ` (/) ) )
27 26 fveq2d 
 |-  ( y e. ( NN0 ^m 1o ) -> ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = ( A ` ( y ` (/) ) ) )
28 27 adantl 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ y e. ( NN0 ^m 1o ) ) -> ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = ( A ` ( y ` (/) ) ) )
29 5 fvcoe1 
 |-  ( ( F e. B /\ y e. ( NN0 ^m 1o ) ) -> ( F ` y ) = ( A ` ( y ` (/) ) ) )
30 29 adantlr 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ y e. ( NN0 ^m 1o ) ) -> ( F ` y ) = ( A ` ( y ` (/) ) ) )
31 28 30 eqtr4d 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ y e. ( NN0 ^m 1o ) ) -> ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = ( F ` y ) )
32 31 eqeq1d 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ y e. ( NN0 ^m 1o ) ) -> ( ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = .0. <-> ( F ` y ) = .0. ) )
33 32 imbi2d 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ y e. ( NN0 ^m 1o ) ) -> ( ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = .0. ) <-> ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( F ` y ) = .0. ) ) )
34 33 ralbidva 
 |-  ( ( F e. B /\ G e. RR* ) -> ( A. y e. ( NN0 ^m 1o ) ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( A ` ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) ) = .0. ) <-> A. y e. ( NN0 ^m 1o ) ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( F ` y ) = .0. ) ) )
35 23 34 bitr3id 
 |-  ( ( F e. B /\ G e. RR* ) -> ( A. x e. NN0 ( G < x -> ( A ` x ) = .0. ) <-> A. y e. ( NN0 ^m 1o ) ( G < ( ( b e. ( NN0 ^m 1o ) |-> ( b ` (/) ) ) ` y ) -> ( F ` y ) = .0. ) ) )
36 12 35 bitr4d 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> A. x e. NN0 ( G < x -> ( A ` x ) = .0. ) ) )