Metamath Proof Explorer

Theorem mdegleb

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

Ref Expression
Hypotheses mdegval.d 
|- D = ( I mDeg R )
mdegval.p 
|- P = ( I mPoly R )
mdegval.b 
|- B = ( Base ` P )
mdegval.z 
|- .0. = ( 0g ` R )
mdegval.a 
|- A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
mdegval.h 
|- H = ( h e. A |-> ( CCfld gsum h ) )
Assertion mdegleb 
|- ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> A. x e. A ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )

Proof

Step Hyp Ref Expression
1 mdegval.d 
 |-  D = ( I mDeg R )
2 mdegval.p 
 |-  P = ( I mPoly R )
3 mdegval.b 
 |-  B = ( Base ` P )
4 mdegval.z 
 |-  .0. = ( 0g ` R )
5 mdegval.a 
 |-  A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
6 mdegval.h 
 |-  H = ( h e. A |-> ( CCfld gsum h ) )
7 1 2 3 4 5 6 mdegval 
 |-  ( F e. B -> ( D ` F ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )
8 7 adantr 
 |-  ( ( F e. B /\ G e. RR* ) -> ( D ` F ) = sup ( ( H " ( F supp .0. ) ) , RR* , < ) )
9 8 breq1d 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> sup ( ( H " ( F supp .0. ) ) , RR* , < ) <_ G ) )
10 imassrn 
 |-  ( H " ( F supp .0. ) ) C_ ran H
11 2 3 mplrcl 
 |-  ( F e. B -> I e. _V )
12 11 adantr 
 |-  ( ( F e. B /\ G e. RR* ) -> I e. _V )
13 5 6 tdeglem1 
 |-  ( I e. _V -> H : A --> NN0 )
14 12 13 syl 
 |-  ( ( F e. B /\ G e. RR* ) -> H : A --> NN0 )
15 14 frnd 
 |-  ( ( F e. B /\ G e. RR* ) -> ran H C_ NN0 )
16 nn0ssre 
 |-  NN0 C_ RR
17 ressxr 
 |-  RR C_ RR*
18 16 17 sstri 
 |-  NN0 C_ RR*
19 15 18 sstrdi 
 |-  ( ( F e. B /\ G e. RR* ) -> ran H C_ RR* )
20 10 19 sstrid 
 |-  ( ( F e. B /\ G e. RR* ) -> ( H " ( F supp .0. ) ) C_ RR* )
21 supxrleub 
 |-  ( ( ( H " ( F supp .0. ) ) C_ RR* /\ G e. RR* ) -> ( sup ( ( H " ( F supp .0. ) ) , RR* , < ) <_ G <-> A. y e. ( H " ( F supp .0. ) ) y <_ G ) )
22 20 21 sylancom 
 |-  ( ( F e. B /\ G e. RR* ) -> ( sup ( ( H " ( F supp .0. ) ) , RR* , < ) <_ G <-> A. y e. ( H " ( F supp .0. ) ) y <_ G ) )
23 14 ffnd 
 |-  ( ( F e. B /\ G e. RR* ) -> H Fn A )
24 suppssdm 
 |-  ( F supp .0. ) C_ dom F
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 simpl 
 |-  ( ( F e. B /\ G e. RR* ) -> F e. B )
27 2 25 3 5 26 mplelf 
 |-  ( ( F e. B /\ G e. RR* ) -> F : A --> ( Base ` R ) )
28 24 27 fssdm 
 |-  ( ( F e. B /\ G e. RR* ) -> ( F supp .0. ) C_ A )
29 breq1 
 |-  ( y = ( H ` x ) -> ( y <_ G <-> ( H ` x ) <_ G ) )
30 29 ralima 
 |-  ( ( H Fn A /\ ( F supp .0. ) C_ A ) -> ( A. y e. ( H " ( F supp .0. ) ) y <_ G <-> A. x e. ( F supp .0. ) ( H ` x ) <_ G ) )
31 23 28 30 syl2anc 
 |-  ( ( F e. B /\ G e. RR* ) -> ( A. y e. ( H " ( F supp .0. ) ) y <_ G <-> A. x e. ( F supp .0. ) ( H ` x ) <_ G ) )
32 27 ffnd 
 |-  ( ( F e. B /\ G e. RR* ) -> F Fn A )
33 ovex 
 |-  ( NN0 ^m I ) e. _V
34 33 rabex 
 |-  { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } e. _V
35 34 a1i 
 |-  ( ( F e. B /\ G e. RR* ) -> { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin } e. _V )
36 5 35 eqeltrid 
 |-  ( ( F e. B /\ G e. RR* ) -> A e. _V )
37 4 fvexi 
 |-  .0. e. _V
38 37 a1i 
 |-  ( ( F e. B /\ G e. RR* ) -> .0. e. _V )
39 elsuppfn 
 |-  ( ( F Fn A /\ A e. _V /\ .0. e. _V ) -> ( x e. ( F supp .0. ) <-> ( x e. A /\ ( F ` x ) =/= .0. ) ) )
40 fvex 
 |-  ( F ` x ) e. _V
41 40 biantrur 
 |-  ( ( F ` x ) =/= .0. <-> ( ( F ` x ) e. _V /\ ( F ` x ) =/= .0. ) )
42 eldifsn 
 |-  ( ( F ` x ) e. ( _V \ { .0. } ) <-> ( ( F ` x ) e. _V /\ ( F ` x ) =/= .0. ) )
43 41 42 bitr4i 
 |-  ( ( F ` x ) =/= .0. <-> ( F ` x ) e. ( _V \ { .0. } ) )
44 43 a1i 
 |-  ( ( F Fn A /\ A e. _V /\ .0. e. _V ) -> ( ( F ` x ) =/= .0. <-> ( F ` x ) e. ( _V \ { .0. } ) ) )
45 44 anbi2d 
 |-  ( ( F Fn A /\ A e. _V /\ .0. e. _V ) -> ( ( x e. A /\ ( F ` x ) =/= .0. ) <-> ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) ) )
46 39 45 bitrd 
 |-  ( ( F Fn A /\ A e. _V /\ .0. e. _V ) -> ( x e. ( F supp .0. ) <-> ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) ) )
47 32 36 38 46 syl3anc 
 |-  ( ( F e. B /\ G e. RR* ) -> ( x e. ( F supp .0. ) <-> ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) ) )
48 47 imbi1d 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( x e. ( F supp .0. ) -> ( H ` x ) <_ G ) <-> ( ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) -> ( H ` x ) <_ G ) ) )
49 impexp 
 |-  ( ( ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) -> ( H ` x ) <_ G ) <-> ( x e. A -> ( ( F ` x ) e. ( _V \ { .0. } ) -> ( H ` x ) <_ G ) ) )
50 con34b 
 |-  ( ( ( F ` x ) e. ( _V \ { .0. } ) -> ( H ` x ) <_ G ) <-> ( -. ( H ` x ) <_ G -> -. ( F ` x ) e. ( _V \ { .0. } ) ) )
51 simplr 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> G e. RR* )
52 14 ffvelrnda 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( H ` x ) e. NN0 )
53 18 52 sseldi 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( H ` x ) e. RR* )
54 xrltnle 
 |-  ( ( G e. RR* /\ ( H ` x ) e. RR* ) -> ( G < ( H ` x ) <-> -. ( H ` x ) <_ G ) )
55 51 53 54 syl2anc 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( G < ( H ` x ) <-> -. ( H ` x ) <_ G ) )
56 55 bicomd 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( -. ( H ` x ) <_ G <-> G < ( H ` x ) ) )
57 ianor 
 |-  ( -. ( ( F ` x ) e. _V /\ ( F ` x ) =/= .0. ) <-> ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) )
58 57 42 xchnxbir 
 |-  ( -. ( F ` x ) e. ( _V \ { .0. } ) <-> ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) )
59 orcom 
 |-  ( ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) <-> ( -. ( F ` x ) =/= .0. \/ -. ( F ` x ) e. _V ) )
60 40 notnoti 
 |-  -. -. ( F ` x ) e. _V
61 60 biorfi 
 |-  ( -. ( F ` x ) =/= .0. <-> ( -. ( F ` x ) =/= .0. \/ -. ( F ` x ) e. _V ) )
62 nne 
 |-  ( -. ( F ` x ) =/= .0. <-> ( F ` x ) = .0. )
63 59 61 62 3bitr2i 
 |-  ( ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) <-> ( F ` x ) = .0. )
64 63 a1i 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) <-> ( F ` x ) = .0. ) )
65 58 64 syl5bb 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( -. ( F ` x ) e. ( _V \ { .0. } ) <-> ( F ` x ) = .0. ) )
66 56 65 imbi12d 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( ( -. ( H ` x ) <_ G -> -. ( F ` x ) e. ( _V \ { .0. } ) ) <-> ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )
67 50 66 syl5bb 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( ( ( F ` x ) e. ( _V \ { .0. } ) -> ( H ` x ) <_ G ) <-> ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )
68 67 pm5.74da 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( x e. A -> ( ( F ` x ) e. ( _V \ { .0. } ) -> ( H ` x ) <_ G ) ) <-> ( x e. A -> ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) ) )
69 49 68 syl5bb 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) -> ( H ` x ) <_ G ) <-> ( x e. A -> ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) ) )
70 48 69 bitrd 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( x e. ( F supp .0. ) -> ( H ` x ) <_ G ) <-> ( x e. A -> ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) ) )
71 70 ralbidv2 
 |-  ( ( F e. B /\ G e. RR* ) -> ( A. x e. ( F supp .0. ) ( H ` x ) <_ G <-> A. x e. A ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )
72 31 71 bitrd 
 |-  ( ( F e. B /\ G e. RR* ) -> ( A. y e. ( H " ( F supp .0. ) ) y <_ G <-> A. x e. A ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )
73 9 22 72 3bitrd 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> A. x e. A ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )