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 = ( Poly1 ` R )
ply1divalg.d 
|- D = ( deg1 ` R )
ply1divalg.b 
|- B = ( Base ` P )
ply1divalg.m 
|- .- = ( -g ` P )
ply1divalg.z 
|- .0. = ( 0g ` P )
ply1divalg.t 
|- .xb = ( .r ` P )
ply1divalg.r1 
|- ( ph -> R e. Ring )
ply1divalg.f 
|- ( ph -> F e. B )
ply1divalg.g1 
|- ( ph -> G e. B )
ply1divalg.g2 
|- ( ph -> G =/= .0. )
ply1divex.o 
|- .1. = ( 1r ` R )
ply1divex.k 
|- K = ( Base ` R )
ply1divex.u 
|- .x. = ( .r ` R )
ply1divex.i 
|- ( ph -> I e. K )
ply1divex.g3 
|- ( ph -> ( ( ( coe1 ` G ) ` ( D ` G ) ) .x. I ) = .1. )
Assertion ply1divex 
|- ( ph -> E. q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )

Proof

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