Metamath Proof Explorer


Theorem ply1divex

Description: Lemma for ply1divalg : existence part. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses ply1divalg.p P = Poly 1 R
ply1divalg.d D = deg 1 R
ply1divalg.b B = Base P
ply1divalg.m - ˙ = - P
ply1divalg.z 0 ˙ = 0 P
ply1divalg.t ˙ = P
ply1divalg.r1 φ R Ring
ply1divalg.f φ F B
ply1divalg.g1 φ G B
ply1divalg.g2 φ G 0 ˙
ply1divex.o 1 ˙ = 1 R
ply1divex.k K = Base R
ply1divex.u · ˙ = R
ply1divex.i φ I K
ply1divex.g3 φ coe 1 G D G · ˙ I = 1 ˙
Assertion ply1divex φ q B D F - ˙ G ˙ q < D G

Proof

Step Hyp Ref Expression
1 ply1divalg.p P = Poly 1 R
2 ply1divalg.d D = deg 1 R
3 ply1divalg.b B = Base P
4 ply1divalg.m - ˙ = - P
5 ply1divalg.z 0 ˙ = 0 P
6 ply1divalg.t ˙ = P
7 ply1divalg.r1 φ R Ring
8 ply1divalg.f φ F B
9 ply1divalg.g1 φ G B
10 ply1divalg.g2 φ G 0 ˙
11 ply1divex.o 1 ˙ = 1 R
12 ply1divex.k K = Base R
13 ply1divex.u · ˙ = R
14 ply1divex.i φ I K
15 ply1divex.g3 φ coe 1 G D G · ˙ I = 1 ˙
16 fveq2 F = 0 ˙ D F = D 0 ˙
17 16 breq1d F = 0 ˙ D F < D G + d D 0 ˙ < D G + d
18 17 rexbidv F = 0 ˙ d 0 D F < D G + d d 0 D 0 ˙ < D G + d
19 nnssnn0 0
20 7 adantr φ F 0 ˙ R Ring
21 8 adantr φ F 0 ˙ F B
22 simpr φ F 0 ˙ F 0 ˙
23 2 1 5 3 deg1nn0cl R Ring F B F 0 ˙ D F 0
24 20 21 22 23 syl3anc φ F 0 ˙ D F 0
25 24 nn0red φ F 0 ˙ D F
26 2 1 5 3 deg1nn0cl R Ring G B G 0 ˙ D G 0
27 7 9 10 26 syl3anc φ D G 0
28 27 nn0red φ D G
29 28 adantr φ F 0 ˙ D G
30 25 29 resubcld φ F 0 ˙ D F D G
31 arch D F D G d D F D G < d
32 30 31 syl φ F 0 ˙ d D F D G < d
33 ssrexv 0 d D F D G < d d 0 D F D G < d
34 19 32 33 mpsyl φ F 0 ˙ d 0 D F D G < d
35 25 adantr φ F 0 ˙ d 0 D F
36 28 ad2antrr φ F 0 ˙ d 0 D G
37 nn0re d 0 d
38 37 adantl φ F 0 ˙ d 0 d
39 35 36 38 ltsubadd2d φ F 0 ˙ d 0 D F D G < d D F < D G + d
40 39 biimpd φ F 0 ˙ d 0 D F D G < d D F < D G + d
41 40 reximdva φ F 0 ˙ d 0 D F D G < d d 0 D F < D G + d
42 34 41 mpd φ F 0 ˙ d 0 D F < D G + d
43 0nn0 0 0
44 2 1 5 deg1z R Ring D 0 ˙ = −∞
45 7 44 syl φ D 0 ˙ = −∞
46 0re 0
47 readdcl D G 0 D G + 0
48 28 46 47 sylancl φ D G + 0
49 48 mnfltd φ −∞ < D G + 0
50 45 49 eqbrtrd φ D 0 ˙ < D G + 0
51 oveq2 d = 0 D G + d = D G + 0
52 51 breq2d d = 0 D 0 ˙ < D G + d D 0 ˙ < D G + 0
53 52 rspcev 0 0 D 0 ˙ < D G + 0 d 0 D 0 ˙ < D G + d
54 43 50 53 sylancr φ d 0 D 0 ˙ < D G + d
55 18 42 54 pm2.61ne φ d 0 D F < D G + d
56 fveq2 f = F D f = D F
57 56 breq1d f = F D f < D G + d D F < D G + d
58 fvoveq1 f = F D f - ˙ G ˙ q = D F - ˙ G ˙ q
59 58 breq1d f = F D f - ˙ G ˙ q < D G D F - ˙ G ˙ q < D G
60 59 rexbidv f = F q B D f - ˙ G ˙ q < D G q B D F - ˙ G ˙ q < D G
61 57 60 imbi12d f = F D f < D G + d q B D f - ˙ G ˙ q < D G D F < D G + d q B D F - ˙ G ˙ q < D G
62 oveq2 a = 0 D G + a = D G + 0
63 62 breq2d a = 0 D f < D G + a D f < D G + 0
64 63 imbi1d a = 0 D f < D G + a q B D f - ˙ G ˙ q < D G D f < D G + 0 q B D f - ˙ G ˙ q < D G
65 64 ralbidv a = 0 f B D f < D G + a q B D f - ˙ G ˙ q < D G f B D f < D G + 0 q B D f - ˙ G ˙ q < D G
66 65 imbi2d a = 0 φ f B D f < D G + a q B D f - ˙ G ˙ q < D G φ f B D f < D G + 0 q B D f - ˙ G ˙ q < D G
67 oveq2 a = d D G + a = D G + d
68 67 breq2d a = d D f < D G + a D f < D G + d
69 68 imbi1d a = d D f < D G + a q B D f - ˙ G ˙ q < D G D f < D G + d q B D f - ˙ G ˙ q < D G
70 69 ralbidv a = d f B D f < D G + a q B D f - ˙ G ˙ q < D G f B D f < D G + d q B D f - ˙ G ˙ q < D G
71 70 imbi2d a = d φ f B D f < D G + a q B D f - ˙ G ˙ q < D G φ f B D f < D G + d q B D f - ˙ G ˙ q < D G
72 oveq2 a = d + 1 D G + a = D G + d + 1
73 72 breq2d a = d + 1 D f < D G + a D f < D G + d + 1
74 73 imbi1d a = d + 1 D f < D G + a q B D f - ˙ G ˙ q < D G D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
75 74 ralbidv a = d + 1 f B D f < D G + a q B D f - ˙ G ˙ q < D G f B D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
76 75 imbi2d a = d + 1 φ f B D f < D G + a q B D f - ˙ G ˙ q < D G φ f B D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
77 1 ply1ring R Ring P Ring
78 7 77 syl φ P Ring
79 3 5 ring0cl P Ring 0 ˙ B
80 78 79 syl φ 0 ˙ B
81 80 ad2antrr φ f B D f < D G + 0 0 ˙ B
82 3 6 5 ringrz P Ring G B G ˙ 0 ˙ = 0 ˙
83 78 9 82 syl2anc φ G ˙ 0 ˙ = 0 ˙
84 83 oveq2d φ f - ˙ G ˙ 0 ˙ = f - ˙ 0 ˙
85 84 adantr φ f B f - ˙ G ˙ 0 ˙ = f - ˙ 0 ˙
86 ringgrp P Ring P Grp
87 78 86 syl φ P Grp
88 3 5 4 grpsubid1 P Grp f B f - ˙ 0 ˙ = f
89 87 88 sylan φ f B f - ˙ 0 ˙ = f
90 85 89 eqtr2d φ f B f = f - ˙ G ˙ 0 ˙
91 90 fveq2d φ f B D f = D f - ˙ G ˙ 0 ˙
92 27 nn0cnd φ D G
93 92 addid1d φ D G + 0 = D G
94 93 adantr φ f B D G + 0 = D G
95 91 94 breq12d φ f B D f < D G + 0 D f - ˙ G ˙ 0 ˙ < D G
96 95 biimpa φ f B D f < D G + 0 D f - ˙ G ˙ 0 ˙ < D G
97 oveq2 q = 0 ˙ G ˙ q = G ˙ 0 ˙
98 97 oveq2d q = 0 ˙ f - ˙ G ˙ q = f - ˙ G ˙ 0 ˙
99 98 fveq2d q = 0 ˙ D f - ˙ G ˙ q = D f - ˙ G ˙ 0 ˙
100 99 breq1d q = 0 ˙ D f - ˙ G ˙ q < D G D f - ˙ G ˙ 0 ˙ < D G
101 100 rspcev 0 ˙ B D f - ˙ G ˙ 0 ˙ < D G q B D f - ˙ G ˙ q < D G
102 81 96 101 syl2anc φ f B D f < D G + 0 q B D f - ˙ G ˙ q < D G
103 102 ex φ f B D f < D G + 0 q B D f - ˙ G ˙ q < D G
104 103 ralrimiva φ f B D f < D G + 0 q B D f - ˙ G ˙ q < D G
105 nn0addcl D G 0 d 0 D G + d 0
106 27 105 sylan φ d 0 D G + d 0
107 106 adantr φ d 0 g B D g < D G + d + 1 D G + d 0
108 7 ad2antrr φ d 0 g B D g < D G + d + 1 R Ring
109 simprl φ d 0 g B D g < D G + d + 1 g B
110 2 1 3 deg1cl g B D g 0 −∞
111 27 ad2antrr φ d 0 g B D G 0
112 peano2nn0 d 0 d + 1 0
113 112 ad2antlr φ d 0 g B d + 1 0
114 111 113 nn0addcld φ d 0 g B D G + d + 1 0
115 114 nn0zd φ d 0 g B D G + d + 1
116 degltlem1 D g 0 −∞ D G + d + 1 D g < D G + d + 1 D g D G + d + 1 - 1
117 110 115 116 syl2an2 φ d 0 g B D g < D G + d + 1 D g D G + d + 1 - 1
118 117 biimpd φ d 0 g B D g < D G + d + 1 D g D G + d + 1 - 1
119 118 impr φ d 0 g B D g < D G + d + 1 D g D G + d + 1 - 1
120 27 adantr φ d 0 D G 0
121 120 nn0cnd φ d 0 D G
122 nn0cn d 0 d
123 122 adantl φ d 0 d
124 peano2cn d d + 1
125 123 124 syl φ d 0 d + 1
126 1cnd φ d 0 1
127 121 125 126 addsubassd φ d 0 D G + d + 1 - 1 = D G + d + 1 - 1
128 ax-1cn 1
129 pncan d 1 d + 1 - 1 = d
130 123 128 129 sylancl φ d 0 d + 1 - 1 = d
131 130 oveq2d φ d 0 D G + d + 1 - 1 = D G + d
132 127 131 eqtrd φ d 0 D G + d + 1 - 1 = D G + d
133 132 adantr φ d 0 g B D g < D G + d + 1 D G + d + 1 - 1 = D G + d
134 119 133 breqtrd φ d 0 g B D g < D G + d + 1 D g D G + d
135 78 ad2antrr φ d 0 g B P Ring
136 9 ad2antrr φ d 0 g B G B
137 7 ad2antrr φ d 0 g B R Ring
138 14 ad2antrr φ d 0 g B I K
139 eqid coe 1 g = coe 1 g
140 139 3 1 12 coe1f g B coe 1 g : 0 K
141 140 adantl φ d 0 g B coe 1 g : 0 K
142 simplr φ d 0 g B d 0
143 111 142 nn0addcld φ d 0 g B D G + d 0
144 141 143 ffvelrnd φ d 0 g B coe 1 g D G + d K
145 12 13 ringcl R Ring I K coe 1 g D G + d K I · ˙ coe 1 g D G + d K
146 137 138 144 145 syl3anc φ d 0 g B I · ˙ coe 1 g D G + d K
147 eqid var 1 R = var 1 R
148 eqid P = P
149 eqid mulGrp P = mulGrp P
150 eqid mulGrp P = mulGrp P
151 12 1 147 148 149 150 3 ply1tmcl R Ring I · ˙ coe 1 g D G + d K d 0 I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
152 137 146 142 151 syl3anc φ d 0 g B I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
153 3 6 ringcl P Ring G B I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
154 135 136 152 153 syl3anc φ d 0 g B G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
155 154 adantrr φ d 0 g B D g < D G + d + 1 G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
156 111 nn0red φ d 0 g B D G
157 156 leidd φ d 0 g B D G D G
158 2 12 1 147 148 149 150 deg1tmle R Ring I · ˙ coe 1 g D G + d K d 0 D I · ˙ coe 1 g D G + d P d mulGrp P var 1 R d
159 137 146 142 158 syl3anc φ d 0 g B D I · ˙ coe 1 g D G + d P d mulGrp P var 1 R d
160 1 2 137 3 6 136 152 111 142 157 159 deg1mulle2 φ d 0 g B D G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D G + d
161 160 adantrr φ d 0 g B D g < D G + d + 1 D G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D G + d
162 eqid coe 1 G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R = coe 1 G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
163 eqid 0 R = 0 R
164 163 12 1 147 148 149 150 3 6 13 136 137 146 142 111 coe1tmmul2fv φ d 0 g B coe 1 G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R d + D G = coe 1 G D G · ˙ I · ˙ coe 1 g D G + d
165 111 nn0cnd φ d 0 g B D G
166 122 ad2antlr φ d 0 g B d
167 165 166 addcomd φ d 0 g B D G + d = d + D G
168 167 fveq2d φ d 0 g B coe 1 G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D G + d = coe 1 G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R d + D G
169 15 oveq1d φ coe 1 G D G · ˙ I · ˙ coe 1 g D G + d = 1 ˙ · ˙ coe 1 g D G + d
170 169 ad2antrr φ d 0 g B coe 1 G D G · ˙ I · ˙ coe 1 g D G + d = 1 ˙ · ˙ coe 1 g D G + d
171 eqid coe 1 G = coe 1 G
172 171 3 1 12 coe1f G B coe 1 G : 0 K
173 9 172 syl φ coe 1 G : 0 K
174 173 ad2antrr φ d 0 g B coe 1 G : 0 K
175 174 111 ffvelrnd φ d 0 g B coe 1 G D G K
176 12 13 ringass R Ring coe 1 G D G K I K coe 1 g D G + d K coe 1 G D G · ˙ I · ˙ coe 1 g D G + d = coe 1 G D G · ˙ I · ˙ coe 1 g D G + d
177 137 175 138 144 176 syl13anc φ d 0 g B coe 1 G D G · ˙ I · ˙ coe 1 g D G + d = coe 1 G D G · ˙ I · ˙ coe 1 g D G + d
178 12 13 11 ringlidm R Ring coe 1 g D G + d K 1 ˙ · ˙ coe 1 g D G + d = coe 1 g D G + d
179 137 144 178 syl2anc φ d 0 g B 1 ˙ · ˙ coe 1 g D G + d = coe 1 g D G + d
180 170 177 179 3eqtr3rd φ d 0 g B coe 1 g D G + d = coe 1 G D G · ˙ I · ˙ coe 1 g D G + d
181 164 168 180 3eqtr4rd φ d 0 g B coe 1 g D G + d = coe 1 G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D G + d
182 181 adantrr φ d 0 g B D g < D G + d + 1 coe 1 g D G + d = coe 1 G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D G + d
183 2 1 3 4 107 108 109 134 155 161 139 162 182 deg1sublt φ d 0 g B D g < D G + d + 1 D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G + d
184 183 adantlrr φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G + d
185 fveq2 f = g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D f = D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
186 185 breq1d f = g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D f < D G + d D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G + d
187 fvoveq1 f = g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D f - ˙ G ˙ q = D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q
188 187 breq1d f = g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D f - ˙ G ˙ q < D G D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G
189 188 rexbidv f = g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R q B D f - ˙ G ˙ q < D G q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G
190 186 189 imbi12d f = g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D f < D G + d q B D f - ˙ G ˙ q < D G D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G + d q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G
191 simplrr φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 f B D f < D G + d q B D f - ˙ G ˙ q < D G
192 87 ad2antrr φ d 0 g B P Grp
193 simpr φ d 0 g B g B
194 3 4 grpsubcl P Grp g B G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
195 192 193 154 194 syl3anc φ d 0 g B g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
196 195 adantrr φ d 0 g B D g < D G + d + 1 g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
197 196 adantlrr φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
198 190 191 197 rspcdva φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G + d q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G
199 184 198 mpd φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G
200 78 ad3antrrr φ d 0 g B q B P Ring
201 simpr φ d 0 g B q B q B
202 152 adantr φ d 0 g B q B I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
203 eqid + P = + P
204 3 203 ringacl P Ring q B I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
205 200 201 202 204 syl3anc φ d 0 g B q B q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
206 87 ad3antrrr φ d 0 g B q B P Grp
207 simplr φ d 0 g B q B g B
208 154 adantr φ d 0 g B q B G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B
209 9 ad3antrrr φ d 0 g B q B G B
210 3 6 ringcl P Ring G B q B G ˙ q B
211 200 209 201 210 syl3anc φ d 0 g B q B G ˙ q B
212 3 203 4 grpsubsub4 P Grp g B G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B G ˙ q B g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q = g - ˙ G ˙ q + P G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
213 206 207 208 211 212 syl13anc φ d 0 g B q B g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q = g - ˙ G ˙ q + P G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
214 3 203 6 ringdi P Ring G B q B I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R = G ˙ q + P G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
215 200 209 201 202 214 syl13anc φ d 0 g B q B G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R = G ˙ q + P G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
216 215 oveq2d φ d 0 g B q B g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R = g - ˙ G ˙ q + P G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
217 213 216 eqtr4d φ d 0 g B q B g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q = g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
218 217 fveq2d φ d 0 g B q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q = D g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
219 218 breq1d φ d 0 g B q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G D g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G
220 219 biimpd φ d 0 g B q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G D g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G
221 oveq2 r = q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R G ˙ r = G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
222 221 oveq2d r = q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R g - ˙ G ˙ r = g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
223 222 fveq2d r = q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D g - ˙ G ˙ r = D g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R
224 223 breq1d r = q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R D g - ˙ G ˙ r < D G D g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G
225 224 rspcev q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R B D g - ˙ G ˙ q + P I · ˙ coe 1 g D G + d P d mulGrp P var 1 R < D G r B D g - ˙ G ˙ r < D G
226 205 220 225 syl6an φ d 0 g B q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G r B D g - ˙ G ˙ r < D G
227 226 rexlimdva φ d 0 g B q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G r B D g - ˙ G ˙ r < D G
228 227 adantrr φ d 0 g B D g < D G + d + 1 q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G r B D g - ˙ G ˙ r < D G
229 228 adantlrr φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 q B D g - ˙ G ˙ I · ˙ coe 1 g D G + d P d mulGrp P var 1 R - ˙ G ˙ q < D G r B D g - ˙ G ˙ r < D G
230 199 229 mpd φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 r B D g - ˙ G ˙ r < D G
231 230 expr φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 r B D g - ˙ G ˙ r < D G
232 231 ralrimiva φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G g B D g < D G + d + 1 r B D g - ˙ G ˙ r < D G
233 fveq2 g = f D g = D f
234 233 breq1d g = f D g < D G + d + 1 D f < D G + d + 1
235 fvoveq1 g = f D g - ˙ G ˙ r = D f - ˙ G ˙ r
236 235 breq1d g = f D g - ˙ G ˙ r < D G D f - ˙ G ˙ r < D G
237 236 rexbidv g = f r B D g - ˙ G ˙ r < D G r B D f - ˙ G ˙ r < D G
238 oveq2 r = q G ˙ r = G ˙ q
239 238 oveq2d r = q f - ˙ G ˙ r = f - ˙ G ˙ q
240 239 fveq2d r = q D f - ˙ G ˙ r = D f - ˙ G ˙ q
241 240 breq1d r = q D f - ˙ G ˙ r < D G D f - ˙ G ˙ q < D G
242 241 cbvrexvw r B D f - ˙ G ˙ r < D G q B D f - ˙ G ˙ q < D G
243 237 242 bitrdi g = f r B D g - ˙ G ˙ r < D G q B D f - ˙ G ˙ q < D G
244 234 243 imbi12d g = f D g < D G + d + 1 r B D g - ˙ G ˙ r < D G D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
245 244 cbvralvw g B D g < D G + d + 1 r B D g - ˙ G ˙ r < D G f B D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
246 232 245 sylib φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G f B D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
247 246 exp32 φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G f B D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
248 247 com12 d 0 φ f B D f < D G + d q B D f - ˙ G ˙ q < D G f B D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
249 248 a2d d 0 φ f B D f < D G + d q B D f - ˙ G ˙ q < D G φ f B D f < D G + d + 1 q B D f - ˙ G ˙ q < D G
250 66 71 76 71 104 249 nn0ind d 0 φ f B D f < D G + d q B D f - ˙ G ˙ q < D G
251 250 impcom φ d 0 f B D f < D G + d q B D f - ˙ G ˙ q < D G
252 8 adantr φ d 0 F B
253 61 251 252 rspcdva φ d 0 D F < D G + d q B D F - ˙ G ˙ q < D G
254 253 rexlimdva φ d 0 D F < D G + d q B D F - ˙ G ˙ q < D G
255 55 254 mpd φ q B D F - ˙ G ˙ q < D G