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 5 6 tdeglem1 
 |-  H : A --> NN0
12 11 a1i 
 |-  ( ( F e. B /\ G e. RR* ) -> H : A --> NN0 )
13 12 frnd 
 |-  ( ( F e. B /\ G e. RR* ) -> ran H C_ NN0 )
14 nn0ssre 
 |-  NN0 C_ RR
15 ressxr 
 |-  RR C_ RR*
16 14 15 sstri 
 |-  NN0 C_ RR*
17 13 16 sstrdi 
 |-  ( ( F e. B /\ G e. RR* ) -> ran H C_ RR* )
18 10 17 sstrid 
 |-  ( ( F e. B /\ G e. RR* ) -> ( H " ( F supp .0. ) ) C_ RR* )
19 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 ) )
20 18 19 sylancom 
 |-  ( ( F e. B /\ G e. RR* ) -> ( sup ( ( H " ( F supp .0. ) ) , RR* , < ) <_ G <-> A. y e. ( H " ( F supp .0. ) ) y <_ G ) )
21 12 ffnd 
 |-  ( ( F e. B /\ G e. RR* ) -> H Fn A )
22 suppssdm 
 |-  ( F supp .0. ) C_ dom F
23 eqid 
 |-  ( Base ` R ) = ( Base ` R )
24 simpl 
 |-  ( ( F e. B /\ G e. RR* ) -> F e. B )
25 2 23 3 5 24 mplelf 
 |-  ( ( F e. B /\ G e. RR* ) -> F : A --> ( Base ` R ) )
26 22 25 fssdm 
 |-  ( ( F e. B /\ G e. RR* ) -> ( F supp .0. ) C_ A )
27 breq1 
 |-  ( y = ( H ` x ) -> ( y <_ G <-> ( H ` x ) <_ G ) )
28 27 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 ) )
29 21 26 28 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 ) )
30 25 ffnd 
 |-  ( ( F e. B /\ G e. RR* ) -> F Fn A )
31 4 fvexi 
 |-  .0. e. _V
32 31 a1i 
 |-  ( ( F e. B /\ G e. RR* ) -> .0. e. _V )
33 elsuppfng 
 |-  ( ( F Fn A /\ F e. B /\ .0. e. _V ) -> ( x e. ( F supp .0. ) <-> ( x e. A /\ ( F ` x ) =/= .0. ) ) )
34 30 24 32 33 syl3anc 
 |-  ( ( F e. B /\ G e. RR* ) -> ( x e. ( F supp .0. ) <-> ( x e. A /\ ( F ` x ) =/= .0. ) ) )
35 fvex 
 |-  ( F ` x ) e. _V
36 35 biantrur 
 |-  ( ( F ` x ) =/= .0. <-> ( ( F ` x ) e. _V /\ ( F ` x ) =/= .0. ) )
37 eldifsn 
 |-  ( ( F ` x ) e. ( _V \ { .0. } ) <-> ( ( F ` x ) e. _V /\ ( F ` x ) =/= .0. ) )
38 36 37 bitr4i 
 |-  ( ( F ` x ) =/= .0. <-> ( F ` x ) e. ( _V \ { .0. } ) )
39 38 anbi2i 
 |-  ( ( x e. A /\ ( F ` x ) =/= .0. ) <-> ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) )
40 34 39 bitrdi 
 |-  ( ( F e. B /\ G e. RR* ) -> ( x e. ( F supp .0. ) <-> ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) ) )
41 40 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 ) ) )
42 impexp 
 |-  ( ( ( x e. A /\ ( F ` x ) e. ( _V \ { .0. } ) ) -> ( H ` x ) <_ G ) <-> ( x e. A -> ( ( F ` x ) e. ( _V \ { .0. } ) -> ( H ` x ) <_ G ) ) )
43 con34b 
 |-  ( ( ( F ` x ) e. ( _V \ { .0. } ) -> ( H ` x ) <_ G ) <-> ( -. ( H ` x ) <_ G -> -. ( F ` x ) e. ( _V \ { .0. } ) ) )
44 simplr 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> G e. RR* )
45 12 ffvelcdmda 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( H ` x ) e. NN0 )
46 16 45 sselid 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( H ` x ) e. RR* )
47 xrltnle 
 |-  ( ( G e. RR* /\ ( H ` x ) e. RR* ) -> ( G < ( H ` x ) <-> -. ( H ` x ) <_ G ) )
48 44 46 47 syl2anc 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( G < ( H ` x ) <-> -. ( H ` x ) <_ G ) )
49 48 bicomd 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( -. ( H ` x ) <_ G <-> G < ( H ` x ) ) )
50 ianor 
 |-  ( -. ( ( F ` x ) e. _V /\ ( F ` x ) =/= .0. ) <-> ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) )
51 50 37 xchnxbir 
 |-  ( -. ( F ` x ) e. ( _V \ { .0. } ) <-> ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) )
52 orcom 
 |-  ( ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) <-> ( -. ( F ` x ) =/= .0. \/ -. ( F ` x ) e. _V ) )
53 35 notnoti 
 |-  -. -. ( F ` x ) e. _V
54 53 biorfri 
 |-  ( -. ( F ` x ) =/= .0. <-> ( -. ( F ` x ) =/= .0. \/ -. ( F ` x ) e. _V ) )
55 nne 
 |-  ( -. ( F ` x ) =/= .0. <-> ( F ` x ) = .0. )
56 52 54 55 3bitr2i 
 |-  ( ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) <-> ( F ` x ) = .0. )
57 56 a1i 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( ( -. ( F ` x ) e. _V \/ -. ( F ` x ) =/= .0. ) <-> ( F ` x ) = .0. ) )
58 51 57 bitrid 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( -. ( F ` x ) e. ( _V \ { .0. } ) <-> ( F ` x ) = .0. ) )
59 49 58 imbi12d 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( ( -. ( H ` x ) <_ G -> -. ( F ` x ) e. ( _V \ { .0. } ) ) <-> ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )
60 43 59 bitrid 
 |-  ( ( ( F e. B /\ G e. RR* ) /\ x e. A ) -> ( ( ( F ` x ) e. ( _V \ { .0. } ) -> ( H ` x ) <_ G ) <-> ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )
61 60 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. ) ) ) )
62 42 61 bitrid 
 |-  ( ( 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. ) ) ) )
63 41 62 bitrd 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( x e. ( F supp .0. ) -> ( H ` x ) <_ G ) <-> ( x e. A -> ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) ) )
64 63 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. ) ) )
65 29 64 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. ) ) )
66 9 20 65 3bitrd 
 |-  ( ( F e. B /\ G e. RR* ) -> ( ( D ` F ) <_ G <-> A. x e. A ( G < ( H ` x ) -> ( F ` x ) = .0. ) ) )