Metamath Proof Explorer


Theorem plydiveu

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
plydiveu.q φ q Poly S
plydiveu.qd φ R = 0 𝑝 deg R < deg G
plydiveu.t T = F f G × f p
plydiveu.p φ p Poly S
plydiveu.pd φ T = 0 𝑝 deg T < deg G
Assertion plydiveu φ p = q

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 plydiveu.q φ q Poly S
10 plydiveu.qd φ R = 0 𝑝 deg R < deg G
11 plydiveu.t T = F f G × f p
12 plydiveu.p φ p Poly S
13 plydiveu.pd φ T = 0 𝑝 deg T < deg G
14 idd φ p f q = 0 𝑝 p f q = 0 𝑝
15 1 2 3 4 5 6 7 8 plydivlem2 φ q Poly S R Poly S
16 9 15 mpdan φ R Poly S
17 1 2 3 4 5 6 7 11 plydivlem2 φ p Poly S T Poly S
18 12 17 mpdan φ T Poly S
19 16 18 1 2 4 plysub φ R f T Poly S
20 dgrcl R f T Poly S deg R f T 0
21 19 20 syl φ deg R f T 0
22 21 nn0red φ deg R f T
23 dgrcl T Poly S deg T 0
24 18 23 syl φ deg T 0
25 24 nn0red φ deg T
26 dgrcl R Poly S deg R 0
27 16 26 syl φ deg R 0
28 27 nn0red φ deg R
29 25 28 ifcld φ if deg R deg T deg T deg R
30 dgrcl G Poly S deg G 0
31 6 30 syl φ deg G 0
32 31 nn0red φ deg G
33 eqid deg R = deg R
34 eqid deg T = deg T
35 33 34 dgrsub R Poly S T Poly S deg R f T if deg R deg T deg T deg R
36 16 18 35 syl2anc φ deg R f T if deg R deg T deg T deg R
37 eqid coeff T = coeff T
38 34 37 dgrlt T Poly S deg G 0 T = 0 𝑝 deg T < deg G deg T deg G coeff T deg G = 0
39 18 31 38 syl2anc φ T = 0 𝑝 deg T < deg G deg T deg G coeff T deg G = 0
40 13 39 mpbid φ deg T deg G coeff T deg G = 0
41 40 simpld φ deg T deg G
42 eqid coeff R = coeff R
43 33 42 dgrlt R Poly S deg G 0 R = 0 𝑝 deg R < deg G deg R deg G coeff R deg G = 0
44 16 31 43 syl2anc φ R = 0 𝑝 deg R < deg G deg R deg G coeff R deg G = 0
45 10 44 mpbid φ deg R deg G coeff R deg G = 0
46 45 simpld φ deg R deg G
47 breq1 deg T = if deg R deg T deg T deg R deg T deg G if deg R deg T deg T deg R deg G
48 breq1 deg R = if deg R deg T deg T deg R deg R deg G if deg R deg T deg T deg R deg G
49 47 48 ifboth deg T deg G deg R deg G if deg R deg T deg T deg R deg G
50 41 46 49 syl2anc φ if deg R deg T deg T deg R deg G
51 22 29 32 36 50 letrd φ deg R f T deg G
52 51 adantr φ p f q 0 𝑝 deg R f T deg G
53 12 9 1 2 4 plysub φ p f q Poly S
54 dgrcl p f q Poly S deg p f q 0
55 53 54 syl φ deg p f q 0
56 nn0addge1 deg G deg p f q 0 deg G deg G + deg p f q
57 32 55 56 syl2anc φ deg G deg G + deg p f q
58 57 adantr φ p f q 0 𝑝 deg G deg G + deg p f q
59 plyf F Poly S F :
60 5 59 syl φ F :
61 60 ffvelrnda φ z F z
62 6 9 1 2 plymul φ G × f q Poly S
63 plyf G × f q Poly S G × f q :
64 62 63 syl φ G × f q :
65 64 ffvelrnda φ z G × f q z
66 6 12 1 2 plymul φ G × f p Poly S
67 plyf G × f p Poly S G × f p :
68 66 67 syl φ G × f p :
69 68 ffvelrnda φ z G × f p z
70 61 65 69 nnncan1d φ z F z - G × f q z - F z G × f p z = G × f p z G × f q z
71 70 mpteq2dva φ z F z - G × f q z - F z G × f p z = z G × f p z G × f q z
72 cnex V
73 72 a1i φ V
74 61 65 subcld φ z F z G × f q z
75 61 69 subcld φ z F z G × f p z
76 60 feqmptd φ F = z F z
77 64 feqmptd φ G × f q = z G × f q z
78 73 61 65 76 77 offval2 φ F f G × f q = z F z G × f q z
79 8 78 syl5eq φ R = z F z G × f q z
80 68 feqmptd φ G × f p = z G × f p z
81 73 61 69 76 80 offval2 φ F f G × f p = z F z G × f p z
82 11 81 syl5eq φ T = z F z G × f p z
83 73 74 75 79 82 offval2 φ R f T = z F z - G × f q z - F z G × f p z
84 73 69 65 80 77 offval2 φ G × f p f G × f q = z G × f p z G × f q z
85 71 83 84 3eqtr4d φ R f T = G × f p f G × f q
86 plyf G Poly S G :
87 6 86 syl φ G :
88 plyf p Poly S p :
89 12 88 syl φ p :
90 plyf q Poly S q :
91 9 90 syl φ q :
92 subdi x y z x y z = x y x z
93 92 adantl φ x y z x y z = x y x z
94 73 87 89 91 93 caofdi φ G × f p f q = G × f p f G × f q
95 85 94 eqtr4d φ R f T = G × f p f q
96 95 fveq2d φ deg R f T = deg G × f p f q
97 96 adantr φ p f q 0 𝑝 deg R f T = deg G × f p f q
98 6 adantr φ p f q 0 𝑝 G Poly S
99 7 adantr φ p f q 0 𝑝 G 0 𝑝
100 53 adantr φ p f q 0 𝑝 p f q Poly S
101 simpr φ p f q 0 𝑝 p f q 0 𝑝
102 eqid deg G = deg G
103 eqid deg p f q = deg p f q
104 102 103 dgrmul G Poly S G 0 𝑝 p f q Poly S p f q 0 𝑝 deg G × f p f q = deg G + deg p f q
105 98 99 100 101 104 syl22anc φ p f q 0 𝑝 deg G × f p f q = deg G + deg p f q
106 97 105 eqtrd φ p f q 0 𝑝 deg R f T = deg G + deg p f q
107 58 106 breqtrrd φ p f q 0 𝑝 deg G deg R f T
108 22 32 letri3d φ deg R f T = deg G deg R f T deg G deg G deg R f T
109 108 adantr φ p f q 0 𝑝 deg R f T = deg G deg R f T deg G deg G deg R f T
110 52 107 109 mpbir2and φ p f q 0 𝑝 deg R f T = deg G
111 110 fveq2d φ p f q 0 𝑝 coeff R f T deg R f T = coeff R f T deg G
112 42 37 coesub R Poly S T Poly S coeff R f T = coeff R f coeff T
113 16 18 112 syl2anc φ coeff R f T = coeff R f coeff T
114 113 fveq1d φ coeff R f T deg G = coeff R f coeff T deg G
115 42 coef3 R Poly S coeff R : 0
116 ffn coeff R : 0 coeff R Fn 0
117 16 115 116 3syl φ coeff R Fn 0
118 37 coef3 T Poly S coeff T : 0
119 ffn coeff T : 0 coeff T Fn 0
120 18 118 119 3syl φ coeff T Fn 0
121 nn0ex 0 V
122 121 a1i φ 0 V
123 inidm 0 0 = 0
124 45 simprd φ coeff R deg G = 0
125 124 adantr φ deg G 0 coeff R deg G = 0
126 40 simprd φ coeff T deg G = 0
127 126 adantr φ deg G 0 coeff T deg G = 0
128 117 120 122 122 123 125 127 ofval φ deg G 0 coeff R f coeff T deg G = 0 0
129 31 128 mpdan φ coeff R f coeff T deg G = 0 0
130 114 129 eqtrd φ coeff R f T deg G = 0 0
131 0m0e0 0 0 = 0
132 130 131 eqtrdi φ coeff R f T deg G = 0
133 132 adantr φ p f q 0 𝑝 coeff R f T deg G = 0
134 111 133 eqtrd φ p f q 0 𝑝 coeff R f T deg R f T = 0
135 eqid deg R f T = deg R f T
136 eqid coeff R f T = coeff R f T
137 135 136 dgreq0 R f T Poly S R f T = 0 𝑝 coeff R f T deg R f T = 0
138 19 137 syl φ R f T = 0 𝑝 coeff R f T deg R f T = 0
139 138 biimpar φ coeff R f T deg R f T = 0 R f T = 0 𝑝
140 134 139 syldan φ p f q 0 𝑝 R f T = 0 𝑝
141 140 ex φ p f q 0 𝑝 R f T = 0 𝑝
142 plymul0or G Poly S p f q Poly S G × f p f q = 0 𝑝 G = 0 𝑝 p f q = 0 𝑝
143 6 53 142 syl2anc φ G × f p f q = 0 𝑝 G = 0 𝑝 p f q = 0 𝑝
144 95 eqeq1d φ R f T = 0 𝑝 G × f p f q = 0 𝑝
145 7 neneqd φ ¬ G = 0 𝑝
146 biorf ¬ G = 0 𝑝 p f q = 0 𝑝 G = 0 𝑝 p f q = 0 𝑝
147 145 146 syl φ p f q = 0 𝑝 G = 0 𝑝 p f q = 0 𝑝
148 143 144 147 3bitr4d φ R f T = 0 𝑝 p f q = 0 𝑝
149 141 148 sylibd φ p f q 0 𝑝 p f q = 0 𝑝
150 14 149 pm2.61dne φ p f q = 0 𝑝
151 df-0p 0 𝑝 = × 0
152 150 151 eqtrdi φ p f q = × 0
153 ofsubeq0 V p : q : p f q = × 0 p = q
154 72 89 91 153 mp3an2i φ p f q = × 0 p = q
155 152 154 mpbid φ p = q