Metamath Proof Explorer

Theorem mdegmullem

Description: Lemma for mdegmulle2 . (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses mdegaddle.y ⊢Y=ImPolyR
mdegaddle.d ⊢D=ImDegR
mdegaddle.i ⊢φ→I∈V
mdegaddle.r ⊢φ→R∈Ring
mdegmulle2.b ⊢B=BaseY
mdegmulle2.t ⊢·˙=⋅Y
mdegmulle2.f ⊢φ→F∈B
mdegmulle2.g ⊢φ→G∈B
mdegmulle2.j1 ⊢φ→J∈ℕ0
mdegmulle2.k1 ⊢φ→K∈ℕ0
mdegmulle2.j2 ⊢φ→D⁡F≤J
mdegmulle2.k2 ⊢φ→D⁡G≤K
mdegmullem.a ⊢A=a∈ℕ0I|a-1ℕ∈Fin
mdegmullem.h ⊢H=b∈A⟼∑ℂfldb
Assertion mdegmullem ⊢φ→D⁡F·˙G≤J+K

Proof

Step Hyp Ref Expression
1 mdegaddle.y ⊢Y=ImPolyR
2 mdegaddle.d ⊢D=ImDegR
3 mdegaddle.i ⊢φ→I∈V
4 mdegaddle.r ⊢φ→R∈Ring
5 mdegmulle2.b ⊢B=BaseY
6 mdegmulle2.t ⊢·˙=⋅Y
7 mdegmulle2.f ⊢φ→F∈B
8 mdegmulle2.g ⊢φ→G∈B
9 mdegmulle2.j1 ⊢φ→J∈ℕ0
10 mdegmulle2.k1 ⊢φ→K∈ℕ0
11 mdegmulle2.j2 ⊢φ→D⁡F≤J
12 mdegmulle2.k2 ⊢φ→D⁡G≤K
13 mdegmullem.a ⊢A=a∈ℕ0I|a-1ℕ∈Fin
14 mdegmullem.h ⊢H=b∈A⟼∑ℂfldb
15 eqid ⊢⋅R=⋅R
16 1 5 15 6 13 7 8 mplmul ⊢φ→F·˙G=c∈A⟼∑Rd∈e∈A|e≤fcF⁡d⋅RG⁡c−fd
17 16 fveq1d ⊢φ→F·˙G⁡x=c∈A⟼∑Rd∈e∈A|e≤fcF⁡d⋅RG⁡c−fd⁡x
18 17 adantr ⊢φ∧x∈A∧J+K<H⁡x→F·˙G⁡x=c∈A⟼∑Rd∈e∈A|e≤fcF⁡d⋅RG⁡c−fd⁡x
19 breq2 ⊢c=x→e≤fc↔e≤fx
20 19 rabbidv ⊢c=x→e∈A|e≤fc=e∈A|e≤fx
21 fvoveq1 ⊢c=x→G⁡c−fd=G⁡x−fd
22 21 oveq2d ⊢c=x→F⁡d⋅RG⁡c−fd=F⁡d⋅RG⁡x−fd
23 20 22 mpteq12dv ⊢c=x→d∈e∈A|e≤fc⟼F⁡d⋅RG⁡c−fd=d∈e∈A|e≤fx⟼F⁡d⋅RG⁡x−fd
24 23 oveq2d ⊢c=x→∑Rd∈e∈A|e≤fcF⁡d⋅RG⁡c−fd=∑Rd∈e∈A|e≤fxF⁡d⋅RG⁡x−fd
25 eqid ⊢c∈A⟼∑Rd∈e∈A|e≤fcF⁡d⋅RG⁡c−fd=c∈A⟼∑Rd∈e∈A|e≤fcF⁡d⋅RG⁡c−fd
26 ovex ⊢∑Rd∈e∈A|e≤fxF⁡d⋅RG⁡x−fd∈V
27 24 25 26 fvmpt ⊢x∈A→c∈A⟼∑Rd∈e∈A|e≤fcF⁡d⋅RG⁡c−fd⁡x=∑Rd∈e∈A|e≤fxF⁡d⋅RG⁡x−fd
28 27 ad2antrl ⊢φ∧x∈A∧J+K<H⁡x→c∈A⟼∑Rd∈e∈A|e≤fcF⁡d⋅RG⁡c−fd⁡x=∑Rd∈e∈A|e≤fxF⁡d⋅RG⁡x−fd
29 eqid ⊢0R=0R
30 7 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→F∈B
31 elrabi ⊢d∈e∈A|e≤fx→d∈A
32 31 adantl ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→d∈A
33 32 adantrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→d∈A
34 2 1 5 mdegxrcl ⊢F∈B→D⁡F∈ℝ*
35 7 34 syl ⊢φ→D⁡F∈ℝ*
36 35 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→D⁡F∈ℝ*
37 nn0ssre ⊢ℕ0⊆ℝ
38 ressxr ⊢ℝ⊆ℝ*
39 37 38 sstri ⊢ℕ0⊆ℝ*
40 39 9 sselid ⊢φ→J∈ℝ*
41 40 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→J∈ℝ*
42 13 14 tdeglem1 ⊢H:A⟶ℕ0
43 42 a1i ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H:A⟶ℕ0
44 43 32 ffvelcdmd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d∈ℕ0
45 39 44 sselid ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d∈ℝ*
46 36 41 45 3jca ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→D⁡F∈ℝ*∧J∈ℝ*∧H⁡d∈ℝ*
47 46 adantrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→D⁡F∈ℝ*∧J∈ℝ*∧H⁡d∈ℝ*
48 11 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→D⁡F≤J
49 48 anim1i ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→D⁡F≤J∧J<H⁡d
50 49 anasss ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→D⁡F≤J∧J<H⁡d
51 xrlelttr ⊢D⁡F∈ℝ*∧J∈ℝ*∧H⁡d∈ℝ*→D⁡F≤J∧J<H⁡d→D⁡F<H⁡d
52 47 50 51 sylc ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→D⁡F<H⁡d
53 2 1 5 29 13 14 30 33 52 mdeglt ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→F⁡d=0R
54 53 oveq1d ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→F⁡d⋅RG⁡x−fd=0R⋅RG⁡x−fd
55 4 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→R∈Ring
56 eqid ⊢BaseR=BaseR
57 1 56 5 13 8 mplelf ⊢φ→G:A⟶BaseR
58 57 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→G:A⟶BaseR
59 ssrab2 ⊢e∈A|e≤fx⊆A
60 simplrl ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→x∈A
61 eqid ⊢e∈A|e≤fx=e∈A|e≤fx
62 13 61 psrbagconcl ⊢x∈A∧d∈e∈A|e≤fx→x−fd∈e∈A|e≤fx
63 60 62 sylancom ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→x−fd∈e∈A|e≤fx
64 59 63 sselid ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→x−fd∈A
65 58 64 ffvelcdmd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→G⁡x−fd∈BaseR
66 56 15 29 ringlz ⊢R∈Ring∧G⁡x−fd∈BaseR→0R⋅RG⁡x−fd=0R
67 55 65 66 syl2anc ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→0R⋅RG⁡x−fd=0R
68 67 adantrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→0R⋅RG⁡x−fd=0R
69 54 68 eqtrd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→F⁡d⋅RG⁡x−fd=0R
70 69 anassrs ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧J<H⁡d→F⁡d⋅RG⁡x−fd=0R
71 8 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→G∈B
72 64 adantrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→x−fd∈A
73 2 1 5 mdegxrcl ⊢G∈B→D⁡G∈ℝ*
74 8 73 syl ⊢φ→D⁡G∈ℝ*
75 74 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→D⁡G∈ℝ*
76 39 10 sselid ⊢φ→K∈ℝ*
77 76 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→K∈ℝ*
78 43 64 ffvelcdmd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡x−fd∈ℕ0
79 39 78 sselid ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡x−fd∈ℝ*
80 75 77 79 3jca ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→D⁡G∈ℝ*∧K∈ℝ*∧H⁡x−fd∈ℝ*
81 80 adantrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→D⁡G∈ℝ*∧K∈ℝ*∧H⁡x−fd∈ℝ*
82 12 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→D⁡G≤K
83 82 anim1i ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→D⁡G≤K∧K<H⁡x−fd
84 83 anasss ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→D⁡G≤K∧K<H⁡x−fd
85 xrlelttr ⊢D⁡G∈ℝ*∧K∈ℝ*∧H⁡x−fd∈ℝ*→D⁡G≤K∧K<H⁡x−fd→D⁡G<H⁡x−fd
86 81 84 85 sylc ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→D⁡G<H⁡x−fd
87 2 1 5 29 13 14 71 72 86 mdeglt ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→G⁡x−fd=0R
88 87 oveq2d ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→F⁡d⋅RG⁡x−fd=F⁡d⋅R0R
89 1 56 5 13 7 mplelf ⊢φ→F:A⟶BaseR
90 89 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→F:A⟶BaseR
91 90 32 ffvelcdmd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→F⁡d∈BaseR
92 56 15 29 ringrz ⊢R∈Ring∧F⁡d∈BaseR→F⁡d⋅R0R=0R
93 55 91 92 syl2anc ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→F⁡d⋅R0R=0R
94 93 adantrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→F⁡d⋅R0R=0R
95 88 94 eqtrd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→F⁡d⋅RG⁡x−fd=0R
96 95 anassrs ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx∧K<H⁡x−fd→F⁡d⋅RG⁡x−fd=0R
97 simplrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→J+K<H⁡x
98 44 nn0red ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d∈ℝ
99 78 nn0red ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡x−fd∈ℝ
100 9 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→J∈ℕ0
101 100 nn0red ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→J∈ℝ
102 10 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→K∈ℕ0
103 102 nn0red ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→K∈ℝ
104 le2add ⊢H⁡d∈ℝ∧H⁡x−fd∈ℝ∧J∈ℝ∧K∈ℝ→H⁡d≤J∧H⁡x−fd≤K→H⁡d+H⁡x−fd≤J+K
105 98 99 101 103 104 syl22anc ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d≤J∧H⁡x−fd≤K→H⁡d+H⁡x−fd≤J+K
106 13 14 tdeglem3 ⊢d∈A∧x−fd∈A→H⁡d+fx−fd=H⁡d+H⁡x−fd
107 32 64 106 syl2anc ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d+fx−fd=H⁡d+H⁡x−fd
108 3 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→I∈V
109 13 psrbagf ⊢d∈A→d:I⟶ℕ0
110 109 3ad2ant2 ⊢I∈V∧d∈A∧x∈A→d:I⟶ℕ0
111 110 ffvelcdmda ⊢I∈V∧d∈A∧x∈A∧b∈I→d⁡b∈ℕ0
112 111 nn0cnd ⊢I∈V∧d∈A∧x∈A∧b∈I→d⁡b∈ℂ
113 13 psrbagf ⊢x∈A→x:I⟶ℕ0
114 113 3ad2ant3 ⊢I∈V∧d∈A∧x∈A→x:I⟶ℕ0
115 114 ffvelcdmda ⊢I∈V∧d∈A∧x∈A∧b∈I→x⁡b∈ℕ0
116 115 nn0cnd ⊢I∈V∧d∈A∧x∈A∧b∈I→x⁡b∈ℂ
117 112 116 pncan3d ⊢I∈V∧d∈A∧x∈A∧b∈I→d⁡b+x⁡b-d⁡b=x⁡b
118 117 mpteq2dva ⊢I∈V∧d∈A∧x∈A→b∈I⟼d⁡b+x⁡b-d⁡b=b∈I⟼x⁡b
119 simp1 ⊢I∈V∧d∈A∧x∈A→I∈V
120 fvexd ⊢I∈V∧d∈A∧x∈A∧b∈I→d⁡b∈V
121 ovexd ⊢I∈V∧d∈A∧x∈A∧b∈I→x⁡b−d⁡b∈V
122 110 feqmptd ⊢I∈V∧d∈A∧x∈A→d=b∈I⟼d⁡b
123 fvexd ⊢I∈V∧d∈A∧x∈A∧b∈I→x⁡b∈V
124 114 feqmptd ⊢I∈V∧d∈A∧x∈A→x=b∈I⟼x⁡b
125 119 123 120 124 122 offval2 ⊢I∈V∧d∈A∧x∈A→x−fd=b∈I⟼x⁡b−d⁡b
126 119 120 121 122 125 offval2 ⊢I∈V∧d∈A∧x∈A→d+fx−fd=b∈I⟼d⁡b+x⁡b-d⁡b
127 118 126 124 3eqtr4d ⊢I∈V∧d∈A∧x∈A→d+fx−fd=x
128 108 32 60 127 syl3anc ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→d+fx−fd=x
129 128 fveq2d ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d+fx−fd=H⁡x
130 107 129 eqtr3d ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d+H⁡x−fd=H⁡x
131 130 breq1d ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d+H⁡x−fd≤J+K↔H⁡x≤J+K
132 105 131 sylibd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d≤J∧H⁡x−fd≤K→H⁡x≤J+K
133 98 101 lenltd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d≤J↔¬J<H⁡d
134 99 103 lenltd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡x−fd≤K↔¬K<H⁡x−fd
135 133 134 anbi12d ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d≤J∧H⁡x−fd≤K↔¬J<H⁡d∧¬K<H⁡x−fd
136 ioran ⊢¬J<H⁡d∨K<H⁡x−fd↔¬J<H⁡d∧¬K<H⁡x−fd
137 135 136 bitr4di ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡d≤J∧H⁡x−fd≤K↔¬J<H⁡d∨K<H⁡x−fd
138 43 60 ffvelcdmd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡x∈ℕ0
139 138 nn0red ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡x∈ℝ
140 9 10 nn0addcld ⊢φ→J+K∈ℕ0
141 140 ad2antrr ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→J+K∈ℕ0
142 141 nn0red ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→J+K∈ℝ
143 139 142 lenltd ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→H⁡x≤J+K↔¬J+K<H⁡x
144 132 137 143 3imtr3d ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→¬J<H⁡d∨K<H⁡x−fd→¬J+K<H⁡x
145 97 144 mt4d ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→J<H⁡d∨K<H⁡x−fd
146 70 96 145 mpjaodan ⊢φ∧x∈A∧J+K<H⁡x∧d∈e∈A|e≤fx→F⁡d⋅RG⁡x−fd=0R
147 146 mpteq2dva ⊢φ∧x∈A∧J+K<H⁡x→d∈e∈A|e≤fx⟼F⁡d⋅RG⁡x−fd=d∈e∈A|e≤fx⟼0R
148 147 oveq2d ⊢φ∧x∈A∧J+K<H⁡x→∑Rd∈e∈A|e≤fxF⁡d⋅RG⁡x−fd=∑Rd∈e∈A|e≤fx0R
149 ringmnd ⊢R∈Ring→R∈Mnd
150 4 149 syl ⊢φ→R∈Mnd
151 150 adantr ⊢φ∧x∈A∧J+K<H⁡x→R∈Mnd
152 ovex ⊢ℕ0I∈V
153 13 152 rab2ex ⊢e∈A|e≤fx∈V
154 29 gsumz ⊢R∈Mnd∧e∈A|e≤fx∈V→∑Rd∈e∈A|e≤fx0R=0R
155 151 153 154 sylancl ⊢φ∧x∈A∧J+K<H⁡x→∑Rd∈e∈A|e≤fx0R=0R
156 148 155 eqtrd ⊢φ∧x∈A∧J+K<H⁡x→∑Rd∈e∈A|e≤fxF⁡d⋅RG⁡x−fd=0R
157 18 28 156 3eqtrd ⊢φ∧x∈A∧J+K<H⁡x→F·˙G⁡x=0R
158 157 expr ⊢φ∧x∈A→J+K<H⁡x→F·˙G⁡x=0R
159 158 ralrimiva ⊢φ→∀x∈AJ+K<H⁡x→F·˙G⁡x=0R
160 1 mplring ⊢I∈V∧R∈Ring→Y∈Ring
161 3 4 160 syl2anc ⊢φ→Y∈Ring
162 5 6 ringcl ⊢Y∈Ring∧F∈B∧G∈B→F·˙G∈B
163 161 7 8 162 syl3anc ⊢φ→F·˙G∈B
164 39 140 sselid ⊢φ→J+K∈ℝ*
165 2 1 5 29 13 14 mdegleb ⊢F·˙G∈B∧J+K∈ℝ*→D⁡F·˙G≤J+K↔∀x∈AJ+K<H⁡x→F·˙G⁡x=0R
166 163 164 165 syl2anc ⊢φ→D⁡F·˙G≤J+K↔∀x∈AJ+K<H⁡x→F·˙G⁡x=0R
167 159 166 mpbird ⊢φ→D⁡F·˙G≤J+K