# 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}\mathrm{mDeg}{R}$
mdegval.p ${⊢}{P}={I}\mathrm{mPoly}{R}$
mdegval.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
mdegval.z
mdegval.a ${⊢}{A}=\left\{{m}\in \left({{ℕ}_{0}}^{{I}}\right)|{{m}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
mdegval.h ${⊢}{H}=\left({h}\in {A}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}{h}\right)$
Assertion mdegleb

### Proof

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