Metamath Proof Explorer


Theorem plydivex

Description: Lemma for plydivalg . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plydiv.pl φ x S y S x + y S
plydiv.tm φ x S y S x y S
plydiv.rc φ x S x 0 1 x S
plydiv.m1 φ 1 S
plydiv.f φ F Poly S
plydiv.g φ G Poly S
plydiv.z φ G 0 𝑝
plydiv.r R = F f G × f q
Assertion plydivex φ q Poly S R = 0 𝑝 deg R < deg G

Proof

Step Hyp Ref Expression
1 plydiv.pl φ x S y S x + y S
2 plydiv.tm φ x S y S x y S
3 plydiv.rc φ x S x 0 1 x S
4 plydiv.m1 φ 1 S
5 plydiv.f φ F Poly S
6 plydiv.g φ G Poly S
7 plydiv.z φ G 0 𝑝
8 plydiv.r R = F f G × f q
9 dgrcl F Poly S deg F 0
10 5 9 syl φ deg F 0
11 10 nn0red φ deg F
12 dgrcl G Poly S deg G 0
13 6 12 syl φ deg G 0
14 13 nn0red φ deg G
15 11 14 resubcld φ deg F deg G
16 arch deg F deg G d deg F deg G < d
17 15 16 syl φ d deg F deg G < d
18 olc deg F deg G < d F = 0 𝑝 deg F deg G < d
19 eqeq1 f = F f = 0 𝑝 F = 0 𝑝
20 fveq2 f = F deg f = deg F
21 20 oveq1d f = F deg f deg G = deg F deg G
22 21 breq1d f = F deg f deg G < d deg F deg G < d
23 19 22 orbi12d f = F f = 0 𝑝 deg f deg G < d F = 0 𝑝 deg F deg G < d
24 oveq1 f = F f f G × f q = F f G × f q
25 24 8 eqtr4di f = F f f G × f q = R
26 25 eqeq1d f = F f f G × f q = 0 𝑝 R = 0 𝑝
27 25 fveq2d f = F deg f f G × f q = deg R
28 27 breq1d f = F deg f f G × f q < deg G deg R < deg G
29 26 28 orbi12d f = F f f G × f q = 0 𝑝 deg f f G × f q < deg G R = 0 𝑝 deg R < deg G
30 29 rexbidv f = F q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G q Poly S R = 0 𝑝 deg R < deg G
31 23 30 imbi12d f = F f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G F = 0 𝑝 deg F deg G < d q Poly S R = 0 𝑝 deg R < deg G
32 nnnn0 d d 0
33 breq2 x = 0 deg f deg G < x deg f deg G < 0
34 33 orbi2d x = 0 f = 0 𝑝 deg f deg G < x f = 0 𝑝 deg f deg G < 0
35 34 imbi1d x = 0 f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f = 0 𝑝 deg f deg G < 0 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
36 35 ralbidv x = 0 f Poly S f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < 0 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
37 36 imbi2d x = 0 φ f Poly S f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G φ f Poly S f = 0 𝑝 deg f deg G < 0 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
38 breq2 x = d deg f deg G < x deg f deg G < d
39 38 orbi2d x = d f = 0 𝑝 deg f deg G < x f = 0 𝑝 deg f deg G < d
40 39 imbi1d x = d f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
41 40 ralbidv x = d f Poly S f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
42 41 imbi2d x = d φ f Poly S f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G φ f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
43 breq2 x = d + 1 deg f deg G < x deg f deg G < d + 1
44 43 orbi2d x = d + 1 f = 0 𝑝 deg f deg G < x f = 0 𝑝 deg f deg G < d + 1
45 44 imbi1d x = d + 1 f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
46 45 ralbidv x = d + 1 f Poly S f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
47 46 imbi2d x = d + 1 φ f Poly S f = 0 𝑝 deg f deg G < x q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G φ f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
48 1 adantlr φ f Poly S f = 0 𝑝 deg f deg G < 0 x S y S x + y S
49 2 adantlr φ f Poly S f = 0 𝑝 deg f deg G < 0 x S y S x y S
50 3 adantlr φ f Poly S f = 0 𝑝 deg f deg G < 0 x S x 0 1 x S
51 4 adantr φ f Poly S f = 0 𝑝 deg f deg G < 0 1 S
52 simprl φ f Poly S f = 0 𝑝 deg f deg G < 0 f Poly S
53 6 adantr φ f Poly S f = 0 𝑝 deg f deg G < 0 G Poly S
54 7 adantr φ f Poly S f = 0 𝑝 deg f deg G < 0 G 0 𝑝
55 eqid f f G × f q = f f G × f q
56 simprr φ f Poly S f = 0 𝑝 deg f deg G < 0 f = 0 𝑝 deg f deg G < 0
57 48 49 50 51 52 53 54 55 56 plydivlem3 φ f Poly S f = 0 𝑝 deg f deg G < 0 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
58 57 expr φ f Poly S f = 0 𝑝 deg f deg G < 0 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
59 58 ralrimiva φ f Poly S f = 0 𝑝 deg f deg G < 0 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
60 eqeq1 f = g f = 0 𝑝 g = 0 𝑝
61 fveq2 f = g deg f = deg g
62 61 oveq1d f = g deg f deg G = deg g deg G
63 62 breq1d f = g deg f deg G < d deg g deg G < d
64 60 63 orbi12d f = g f = 0 𝑝 deg f deg G < d g = 0 𝑝 deg g deg G < d
65 oveq1 f = g f f G × f q = g f G × f q
66 65 eqeq1d f = g f f G × f q = 0 𝑝 g f G × f q = 0 𝑝
67 65 fveq2d f = g deg f f G × f q = deg g f G × f q
68 67 breq1d f = g deg f f G × f q < deg G deg g f G × f q < deg G
69 66 68 orbi12d f = g f f G × f q = 0 𝑝 deg f f G × f q < deg G g f G × f q = 0 𝑝 deg g f G × f q < deg G
70 69 rexbidv f = g q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G
71 64 70 imbi12d f = g f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G
72 71 cbvralvw f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G
73 simplll φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d φ
74 73 1 sylan φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d x S y S x + y S
75 73 2 sylan φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d x S y S x y S
76 73 3 sylan φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d x S x 0 1 x S
77 73 4 syl φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d 1 S
78 simplr φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d f Poly S
79 73 6 syl φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d G Poly S
80 73 7 syl φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d G 0 𝑝
81 simpllr φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d d 0
82 simprrr φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d deg f deg G = d
83 simprrl φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d f 0 𝑝
84 eqid g f G × f p = g f G × f p
85 oveq1 w = z w d = z d
86 85 oveq2d w = z coeff f deg f coeff G deg G w d = coeff f deg f coeff G deg G z d
87 86 cbvmptv w coeff f deg f coeff G deg G w d = z coeff f deg f coeff G deg G z d
88 simprl φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G
89 oveq2 q = p G × f q = G × f p
90 89 oveq2d q = p g f G × f q = g f G × f p
91 90 eqeq1d q = p g f G × f q = 0 𝑝 g f G × f p = 0 𝑝
92 90 fveq2d q = p deg g f G × f q = deg g f G × f p
93 92 breq1d q = p deg g f G × f q < deg G deg g f G × f p < deg G
94 91 93 orbi12d q = p g f G × f q = 0 𝑝 deg g f G × f q < deg G g f G × f p = 0 𝑝 deg g f G × f p < deg G
95 94 cbvrexvw q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G p Poly S g f G × f p = 0 𝑝 deg g f G × f p < deg G
96 95 imbi2i g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G g = 0 𝑝 deg g deg G < d p Poly S g f G × f p = 0 𝑝 deg g f G × f p < deg G
97 96 ralbii g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G g Poly S g = 0 𝑝 deg g deg G < d p Poly S g f G × f p = 0 𝑝 deg g f G × f p < deg G
98 88 97 sylib φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d g Poly S g = 0 𝑝 deg g deg G < d p Poly S g f G × f p = 0 𝑝 deg g f G × f p < deg G
99 eqid coeff f = coeff f
100 eqid coeff G = coeff G
101 eqid deg f = deg f
102 eqid deg G = deg G
103 74 75 76 77 78 79 80 55 81 82 83 84 87 98 99 100 101 102 plydivlem4 φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
104 103 exp32 φ d 0 f Poly S g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
105 104 ralrimdva φ d 0 g Poly S g = 0 𝑝 deg g deg G < d q Poly S g f G × f q = 0 𝑝 deg g f G × f q < deg G f Poly S f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
106 72 105 syl5bi φ d 0 f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
107 106 ancld φ d 0 f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
108 dgrcl f Poly S deg f 0
109 108 adantl φ d 0 f Poly S deg f 0
110 109 nn0zd φ d 0 f Poly S deg f
111 6 ad2antrr φ d 0 f Poly S G Poly S
112 111 12 syl φ d 0 f Poly S deg G 0
113 112 nn0zd φ d 0 f Poly S deg G
114 110 113 zsubcld φ d 0 f Poly S deg f deg G
115 nn0z d 0 d
116 115 ad2antlr φ d 0 f Poly S d
117 zleltp1 deg f deg G d deg f deg G d deg f deg G < d + 1
118 114 116 117 syl2anc φ d 0 f Poly S deg f deg G d deg f deg G < d + 1
119 114 zred φ d 0 f Poly S deg f deg G
120 nn0re d 0 d
121 120 ad2antlr φ d 0 f Poly S d
122 119 121 leloed φ d 0 f Poly S deg f deg G d deg f deg G < d deg f deg G = d
123 118 122 bitr3d φ d 0 f Poly S deg f deg G < d + 1 deg f deg G < d deg f deg G = d
124 123 orbi2d φ d 0 f Poly S f = 0 𝑝 deg f deg G < d + 1 f = 0 𝑝 deg f deg G < d deg f deg G = d
125 pm5.63 f = 0 𝑝 deg f deg G = d f = 0 𝑝 ¬ f = 0 𝑝 deg f deg G = d
126 df-ne f 0 𝑝 ¬ f = 0 𝑝
127 126 anbi1i f 0 𝑝 deg f deg G = d ¬ f = 0 𝑝 deg f deg G = d
128 127 orbi2i f = 0 𝑝 f 0 𝑝 deg f deg G = d f = 0 𝑝 ¬ f = 0 𝑝 deg f deg G = d
129 125 128 bitr4i f = 0 𝑝 deg f deg G = d f = 0 𝑝 f 0 𝑝 deg f deg G = d
130 129 orbi2i deg f deg G < d f = 0 𝑝 deg f deg G = d deg f deg G < d f = 0 𝑝 f 0 𝑝 deg f deg G = d
131 or12 f = 0 𝑝 deg f deg G < d deg f deg G = d deg f deg G < d f = 0 𝑝 deg f deg G = d
132 or12 f = 0 𝑝 deg f deg G < d f 0 𝑝 deg f deg G = d deg f deg G < d f = 0 𝑝 f 0 𝑝 deg f deg G = d
133 130 131 132 3bitr4i f = 0 𝑝 deg f deg G < d deg f deg G = d f = 0 𝑝 deg f deg G < d f 0 𝑝 deg f deg G = d
134 orass f = 0 𝑝 deg f deg G < d f 0 𝑝 deg f deg G = d f = 0 𝑝 deg f deg G < d f 0 𝑝 deg f deg G = d
135 133 134 bitr4i f = 0 𝑝 deg f deg G < d deg f deg G = d f = 0 𝑝 deg f deg G < d f 0 𝑝 deg f deg G = d
136 124 135 bitrdi φ d 0 f Poly S f = 0 𝑝 deg f deg G < d + 1 f = 0 𝑝 deg f deg G < d f 0 𝑝 deg f deg G = d
137 136 imbi1d φ d 0 f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f = 0 𝑝 deg f deg G < d f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
138 jaob f = 0 𝑝 deg f deg G < d f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
139 137 138 bitrdi φ d 0 f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
140 139 ralbidva φ d 0 f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
141 r19.26 f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
142 140 141 bitrdi φ d 0 f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f 0 𝑝 deg f deg G = d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
143 107 142 sylibrd φ d 0 f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
144 143 expcom d 0 φ f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
145 144 a2d d 0 φ f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G φ f Poly S f = 0 𝑝 deg f deg G < d + 1 q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
146 37 42 47 42 59 145 nn0ind d 0 φ f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
147 32 146 syl d φ f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
148 147 impcom φ d f Poly S f = 0 𝑝 deg f deg G < d q Poly S f f G × f q = 0 𝑝 deg f f G × f q < deg G
149 5 adantr φ d F Poly S
150 31 148 149 rspcdva φ d F = 0 𝑝 deg F deg G < d q Poly S R = 0 𝑝 deg R < deg G
151 18 150 syl5 φ d deg F deg G < d q Poly S R = 0 𝑝 deg R < deg G
152 151 rexlimdva φ d deg F deg G < d q Poly S R = 0 𝑝 deg R < deg G
153 17 152 mpd φ q Poly S R = 0 𝑝 deg R < deg G