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 ) ) |