Step |
Hyp |
Ref |
Expression |
1 |
|
hbtlem.p |
|- P = ( Poly1 ` R ) |
2 |
|
hbtlem.u |
|- U = ( LIdeal ` P ) |
3 |
|
hbtlem.s |
|- S = ( ldgIdlSeq ` R ) |
4 |
|
hbtlem3.r |
|- ( ph -> R e. Ring ) |
5 |
|
hbtlem3.i |
|- ( ph -> I e. U ) |
6 |
|
hbtlem3.j |
|- ( ph -> J e. U ) |
7 |
|
hbtlem3.ij |
|- ( ph -> I C_ J ) |
8 |
|
hbtlem5.e |
|- ( ph -> A. x e. NN0 ( ( S ` J ) ` x ) C_ ( ( S ` I ) ` x ) ) |
9 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
10 |
9 2
|
lidlss |
|- ( J e. U -> J C_ ( Base ` P ) ) |
11 |
6 10
|
syl |
|- ( ph -> J C_ ( Base ` P ) ) |
12 |
11
|
sselda |
|- ( ( ph /\ a e. J ) -> a e. ( Base ` P ) ) |
13 |
|
eqid |
|- ( deg1 ` R ) = ( deg1 ` R ) |
14 |
13 1 9
|
deg1cl |
|- ( a e. ( Base ` P ) -> ( ( deg1 ` R ) ` a ) e. ( NN0 u. { -oo } ) ) |
15 |
12 14
|
syl |
|- ( ( ph /\ a e. J ) -> ( ( deg1 ` R ) ` a ) e. ( NN0 u. { -oo } ) ) |
16 |
|
elun |
|- ( ( ( deg1 ` R ) ` a ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` R ) ` a ) e. NN0 \/ ( ( deg1 ` R ) ` a ) e. { -oo } ) ) |
17 |
|
nnssnn0 |
|- NN C_ NN0 |
18 |
|
nn0re |
|- ( ( ( deg1 ` R ) ` a ) e. NN0 -> ( ( deg1 ` R ) ` a ) e. RR ) |
19 |
|
arch |
|- ( ( ( deg1 ` R ) ` a ) e. RR -> E. b e. NN ( ( deg1 ` R ) ` a ) < b ) |
20 |
18 19
|
syl |
|- ( ( ( deg1 ` R ) ` a ) e. NN0 -> E. b e. NN ( ( deg1 ` R ) ` a ) < b ) |
21 |
|
ssrexv |
|- ( NN C_ NN0 -> ( E. b e. NN ( ( deg1 ` R ) ` a ) < b -> E. b e. NN0 ( ( deg1 ` R ) ` a ) < b ) ) |
22 |
17 20 21
|
mpsyl |
|- ( ( ( deg1 ` R ) ` a ) e. NN0 -> E. b e. NN0 ( ( deg1 ` R ) ` a ) < b ) |
23 |
|
elsni |
|- ( ( ( deg1 ` R ) ` a ) e. { -oo } -> ( ( deg1 ` R ) ` a ) = -oo ) |
24 |
|
0nn0 |
|- 0 e. NN0 |
25 |
|
mnflt0 |
|- -oo < 0 |
26 |
|
breq2 |
|- ( b = 0 -> ( -oo < b <-> -oo < 0 ) ) |
27 |
26
|
rspcev |
|- ( ( 0 e. NN0 /\ -oo < 0 ) -> E. b e. NN0 -oo < b ) |
28 |
24 25 27
|
mp2an |
|- E. b e. NN0 -oo < b |
29 |
|
breq1 |
|- ( ( ( deg1 ` R ) ` a ) = -oo -> ( ( ( deg1 ` R ) ` a ) < b <-> -oo < b ) ) |
30 |
29
|
rexbidv |
|- ( ( ( deg1 ` R ) ` a ) = -oo -> ( E. b e. NN0 ( ( deg1 ` R ) ` a ) < b <-> E. b e. NN0 -oo < b ) ) |
31 |
28 30
|
mpbiri |
|- ( ( ( deg1 ` R ) ` a ) = -oo -> E. b e. NN0 ( ( deg1 ` R ) ` a ) < b ) |
32 |
23 31
|
syl |
|- ( ( ( deg1 ` R ) ` a ) e. { -oo } -> E. b e. NN0 ( ( deg1 ` R ) ` a ) < b ) |
33 |
22 32
|
jaoi |
|- ( ( ( ( deg1 ` R ) ` a ) e. NN0 \/ ( ( deg1 ` R ) ` a ) e. { -oo } ) -> E. b e. NN0 ( ( deg1 ` R ) ` a ) < b ) |
34 |
16 33
|
sylbi |
|- ( ( ( deg1 ` R ) ` a ) e. ( NN0 u. { -oo } ) -> E. b e. NN0 ( ( deg1 ` R ) ` a ) < b ) |
35 |
15 34
|
syl |
|- ( ( ph /\ a e. J ) -> E. b e. NN0 ( ( deg1 ` R ) ` a ) < b ) |
36 |
|
breq2 |
|- ( c = 0 -> ( ( ( deg1 ` R ) ` a ) < c <-> ( ( deg1 ` R ) ` a ) < 0 ) ) |
37 |
36
|
imbi1d |
|- ( c = 0 -> ( ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) <-> ( ( ( deg1 ` R ) ` a ) < 0 -> a e. I ) ) ) |
38 |
37
|
ralbidv |
|- ( c = 0 -> ( A. a e. J ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) <-> A. a e. J ( ( ( deg1 ` R ) ` a ) < 0 -> a e. I ) ) ) |
39 |
38
|
imbi2d |
|- ( c = 0 -> ( ( ph -> A. a e. J ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) ) <-> ( ph -> A. a e. J ( ( ( deg1 ` R ) ` a ) < 0 -> a e. I ) ) ) ) |
40 |
|
breq2 |
|- ( c = b -> ( ( ( deg1 ` R ) ` a ) < c <-> ( ( deg1 ` R ) ` a ) < b ) ) |
41 |
40
|
imbi1d |
|- ( c = b -> ( ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) <-> ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) ) |
42 |
41
|
ralbidv |
|- ( c = b -> ( A. a e. J ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) <-> A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) ) |
43 |
42
|
imbi2d |
|- ( c = b -> ( ( ph -> A. a e. J ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) ) <-> ( ph -> A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) ) ) |
44 |
|
breq2 |
|- ( c = ( b + 1 ) -> ( ( ( deg1 ` R ) ` a ) < c <-> ( ( deg1 ` R ) ` a ) < ( b + 1 ) ) ) |
45 |
44
|
imbi1d |
|- ( c = ( b + 1 ) -> ( ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) <-> ( ( ( deg1 ` R ) ` a ) < ( b + 1 ) -> a e. I ) ) ) |
46 |
45
|
ralbidv |
|- ( c = ( b + 1 ) -> ( A. a e. J ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) <-> A. a e. J ( ( ( deg1 ` R ) ` a ) < ( b + 1 ) -> a e. I ) ) ) |
47 |
|
fveq2 |
|- ( a = d -> ( ( deg1 ` R ) ` a ) = ( ( deg1 ` R ) ` d ) ) |
48 |
47
|
breq1d |
|- ( a = d -> ( ( ( deg1 ` R ) ` a ) < ( b + 1 ) <-> ( ( deg1 ` R ) ` d ) < ( b + 1 ) ) ) |
49 |
|
eleq1 |
|- ( a = d -> ( a e. I <-> d e. I ) ) |
50 |
48 49
|
imbi12d |
|- ( a = d -> ( ( ( ( deg1 ` R ) ` a ) < ( b + 1 ) -> a e. I ) <-> ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) -> d e. I ) ) ) |
51 |
50
|
cbvralvw |
|- ( A. a e. J ( ( ( deg1 ` R ) ` a ) < ( b + 1 ) -> a e. I ) <-> A. d e. J ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) -> d e. I ) ) |
52 |
46 51
|
syl6bb |
|- ( c = ( b + 1 ) -> ( A. a e. J ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) <-> A. d e. J ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) -> d e. I ) ) ) |
53 |
52
|
imbi2d |
|- ( c = ( b + 1 ) -> ( ( ph -> A. a e. J ( ( ( deg1 ` R ) ` a ) < c -> a e. I ) ) <-> ( ph -> A. d e. J ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) -> d e. I ) ) ) ) |
54 |
4
|
adantr |
|- ( ( ph /\ a e. J ) -> R e. Ring ) |
55 |
|
eqid |
|- ( 0g ` P ) = ( 0g ` P ) |
56 |
13 1 55 9
|
deg1lt0 |
|- ( ( R e. Ring /\ a e. ( Base ` P ) ) -> ( ( ( deg1 ` R ) ` a ) < 0 <-> a = ( 0g ` P ) ) ) |
57 |
54 12 56
|
syl2anc |
|- ( ( ph /\ a e. J ) -> ( ( ( deg1 ` R ) ` a ) < 0 <-> a = ( 0g ` P ) ) ) |
58 |
1
|
ply1ring |
|- ( R e. Ring -> P e. Ring ) |
59 |
4 58
|
syl |
|- ( ph -> P e. Ring ) |
60 |
2 55
|
lidl0cl |
|- ( ( P e. Ring /\ I e. U ) -> ( 0g ` P ) e. I ) |
61 |
59 5 60
|
syl2anc |
|- ( ph -> ( 0g ` P ) e. I ) |
62 |
|
eleq1a |
|- ( ( 0g ` P ) e. I -> ( a = ( 0g ` P ) -> a e. I ) ) |
63 |
61 62
|
syl |
|- ( ph -> ( a = ( 0g ` P ) -> a e. I ) ) |
64 |
63
|
adantr |
|- ( ( ph /\ a e. J ) -> ( a = ( 0g ` P ) -> a e. I ) ) |
65 |
57 64
|
sylbid |
|- ( ( ph /\ a e. J ) -> ( ( ( deg1 ` R ) ` a ) < 0 -> a e. I ) ) |
66 |
65
|
ralrimiva |
|- ( ph -> A. a e. J ( ( ( deg1 ` R ) ` a ) < 0 -> a e. I ) ) |
67 |
11
|
3ad2ant2 |
|- ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) -> J C_ ( Base ` P ) ) |
68 |
67
|
sselda |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ d e. J ) -> d e. ( Base ` P ) ) |
69 |
13 1 9
|
deg1cl |
|- ( d e. ( Base ` P ) -> ( ( deg1 ` R ) ` d ) e. ( NN0 u. { -oo } ) ) |
70 |
68 69
|
syl |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ d e. J ) -> ( ( deg1 ` R ) ` d ) e. ( NN0 u. { -oo } ) ) |
71 |
|
simpl1 |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ d e. J ) -> b e. NN0 ) |
72 |
71
|
nn0zd |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ d e. J ) -> b e. ZZ ) |
73 |
|
degltp1le |
|- ( ( ( ( deg1 ` R ) ` d ) e. ( NN0 u. { -oo } ) /\ b e. ZZ ) -> ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) <-> ( ( deg1 ` R ) ` d ) <_ b ) ) |
74 |
70 72 73
|
syl2anc |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ d e. J ) -> ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) <-> ( ( deg1 ` R ) ` d ) <_ b ) ) |
75 |
|
fveq2 |
|- ( x = b -> ( ( S ` J ) ` x ) = ( ( S ` J ) ` b ) ) |
76 |
|
fveq2 |
|- ( x = b -> ( ( S ` I ) ` x ) = ( ( S ` I ) ` b ) ) |
77 |
75 76
|
sseq12d |
|- ( x = b -> ( ( ( S ` J ) ` x ) C_ ( ( S ` I ) ` x ) <-> ( ( S ` J ) ` b ) C_ ( ( S ` I ) ` b ) ) ) |
78 |
77
|
rspcva |
|- ( ( b e. NN0 /\ A. x e. NN0 ( ( S ` J ) ` x ) C_ ( ( S ` I ) ` x ) ) -> ( ( S ` J ) ` b ) C_ ( ( S ` I ) ` b ) ) |
79 |
8 78
|
sylan2 |
|- ( ( b e. NN0 /\ ph ) -> ( ( S ` J ) ` b ) C_ ( ( S ` I ) ` b ) ) |
80 |
4
|
adantl |
|- ( ( b e. NN0 /\ ph ) -> R e. Ring ) |
81 |
6
|
adantl |
|- ( ( b e. NN0 /\ ph ) -> J e. U ) |
82 |
|
simpl |
|- ( ( b e. NN0 /\ ph ) -> b e. NN0 ) |
83 |
1 2 3 13
|
hbtlem1 |
|- ( ( R e. Ring /\ J e. U /\ b e. NN0 ) -> ( ( S ` J ) ` b ) = { c | E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
84 |
80 81 82 83
|
syl3anc |
|- ( ( b e. NN0 /\ ph ) -> ( ( S ` J ) ` b ) = { c | E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
85 |
5
|
adantl |
|- ( ( b e. NN0 /\ ph ) -> I e. U ) |
86 |
1 2 3 13
|
hbtlem1 |
|- ( ( R e. Ring /\ I e. U /\ b e. NN0 ) -> ( ( S ` I ) ` b ) = { c | E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
87 |
80 85 82 86
|
syl3anc |
|- ( ( b e. NN0 /\ ph ) -> ( ( S ` I ) ` b ) = { c | E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
88 |
79 84 87
|
3sstr3d |
|- ( ( b e. NN0 /\ ph ) -> { c | E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } C_ { c | E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
89 |
88
|
3adant3 |
|- ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) -> { c | E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } C_ { c | E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
90 |
89
|
adantr |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) -> { c | E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } C_ { c | E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
91 |
|
simpl |
|- ( ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) -> d e. J ) |
92 |
|
simpr |
|- ( ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) -> ( ( deg1 ` R ) ` d ) <_ b ) |
93 |
|
eqidd |
|- ( ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) -> ( ( coe1 ` d ) ` b ) = ( ( coe1 ` d ) ` b ) ) |
94 |
|
fveq2 |
|- ( e = d -> ( ( deg1 ` R ) ` e ) = ( ( deg1 ` R ) ` d ) ) |
95 |
94
|
breq1d |
|- ( e = d -> ( ( ( deg1 ` R ) ` e ) <_ b <-> ( ( deg1 ` R ) ` d ) <_ b ) ) |
96 |
|
fveq2 |
|- ( e = d -> ( coe1 ` e ) = ( coe1 ` d ) ) |
97 |
96
|
fveq1d |
|- ( e = d -> ( ( coe1 ` e ) ` b ) = ( ( coe1 ` d ) ` b ) ) |
98 |
97
|
eqeq2d |
|- ( e = d -> ( ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) <-> ( ( coe1 ` d ) ` b ) = ( ( coe1 ` d ) ` b ) ) ) |
99 |
95 98
|
anbi12d |
|- ( e = d -> ( ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) <-> ( ( ( deg1 ` R ) ` d ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` d ) ` b ) ) ) ) |
100 |
99
|
rspcev |
|- ( ( d e. J /\ ( ( ( deg1 ` R ) ` d ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` d ) ` b ) ) ) -> E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) |
101 |
91 92 93 100
|
syl12anc |
|- ( ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) -> E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) |
102 |
|
fvex |
|- ( ( coe1 ` d ) ` b ) e. _V |
103 |
|
eqeq1 |
|- ( c = ( ( coe1 ` d ) ` b ) -> ( c = ( ( coe1 ` e ) ` b ) <-> ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) |
104 |
103
|
anbi2d |
|- ( c = ( ( coe1 ` d ) ` b ) -> ( ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) <-> ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) |
105 |
104
|
rexbidv |
|- ( c = ( ( coe1 ` d ) ` b ) -> ( E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) <-> E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) |
106 |
102 105
|
elab |
|- ( ( ( coe1 ` d ) ` b ) e. { c | E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } <-> E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) |
107 |
101 106
|
sylibr |
|- ( ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) -> ( ( coe1 ` d ) ` b ) e. { c | E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
108 |
107
|
adantl |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) -> ( ( coe1 ` d ) ` b ) e. { c | E. e e. J ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
109 |
90 108
|
sseldd |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) -> ( ( coe1 ` d ) ` b ) e. { c | E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } ) |
110 |
104
|
rexbidv |
|- ( c = ( ( coe1 ` d ) ` b ) -> ( E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) <-> E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) |
111 |
102 110
|
elab |
|- ( ( ( coe1 ` d ) ` b ) e. { c | E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } <-> E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) |
112 |
|
simpll2 |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ph ) |
113 |
112 59
|
syl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> P e. Ring ) |
114 |
|
ringgrp |
|- ( P e. Ring -> P e. Grp ) |
115 |
113 114
|
syl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> P e. Grp ) |
116 |
112 11
|
syl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> J C_ ( Base ` P ) ) |
117 |
|
simplrl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> d e. J ) |
118 |
116 117
|
sseldd |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> d e. ( Base ` P ) ) |
119 |
9 2
|
lidlss |
|- ( I e. U -> I C_ ( Base ` P ) ) |
120 |
5 119
|
syl |
|- ( ph -> I C_ ( Base ` P ) ) |
121 |
112 120
|
syl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> I C_ ( Base ` P ) ) |
122 |
|
simprl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> e e. I ) |
123 |
121 122
|
sseldd |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> e e. ( Base ` P ) ) |
124 |
|
eqid |
|- ( +g ` P ) = ( +g ` P ) |
125 |
|
eqid |
|- ( -g ` P ) = ( -g ` P ) |
126 |
9 124 125
|
grpnpcan |
|- ( ( P e. Grp /\ d e. ( Base ` P ) /\ e e. ( Base ` P ) ) -> ( ( d ( -g ` P ) e ) ( +g ` P ) e ) = d ) |
127 |
115 118 123 126
|
syl3anc |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( ( d ( -g ` P ) e ) ( +g ` P ) e ) = d ) |
128 |
5
|
3ad2ant2 |
|- ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) -> I e. U ) |
129 |
128
|
ad2antrr |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> I e. U ) |
130 |
|
simpll1 |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> b e. NN0 ) |
131 |
112 4
|
syl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> R e. Ring ) |
132 |
|
simplrr |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( ( deg1 ` R ) ` d ) <_ b ) |
133 |
|
simprrl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( ( deg1 ` R ) ` e ) <_ b ) |
134 |
|
eqid |
|- ( coe1 ` d ) = ( coe1 ` d ) |
135 |
|
eqid |
|- ( coe1 ` e ) = ( coe1 ` e ) |
136 |
|
simprrr |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) |
137 |
13 1 9 125 130 131 118 132 123 133 134 135 136
|
deg1sublt |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( ( deg1 ` R ) ` ( d ( -g ` P ) e ) ) < b ) |
138 |
112 6
|
syl |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> J e. U ) |
139 |
7
|
3ad2ant2 |
|- ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) -> I C_ J ) |
140 |
139
|
ad2antrr |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> I C_ J ) |
141 |
140 122
|
sseldd |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> e e. J ) |
142 |
2 125
|
lidlsubcl |
|- ( ( ( P e. Ring /\ J e. U ) /\ ( d e. J /\ e e. J ) ) -> ( d ( -g ` P ) e ) e. J ) |
143 |
113 138 117 141 142
|
syl22anc |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( d ( -g ` P ) e ) e. J ) |
144 |
|
simpll3 |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) |
145 |
|
fveq2 |
|- ( a = ( d ( -g ` P ) e ) -> ( ( deg1 ` R ) ` a ) = ( ( deg1 ` R ) ` ( d ( -g ` P ) e ) ) ) |
146 |
145
|
breq1d |
|- ( a = ( d ( -g ` P ) e ) -> ( ( ( deg1 ` R ) ` a ) < b <-> ( ( deg1 ` R ) ` ( d ( -g ` P ) e ) ) < b ) ) |
147 |
|
eleq1 |
|- ( a = ( d ( -g ` P ) e ) -> ( a e. I <-> ( d ( -g ` P ) e ) e. I ) ) |
148 |
146 147
|
imbi12d |
|- ( a = ( d ( -g ` P ) e ) -> ( ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) <-> ( ( ( deg1 ` R ) ` ( d ( -g ` P ) e ) ) < b -> ( d ( -g ` P ) e ) e. I ) ) ) |
149 |
148
|
rspcva |
|- ( ( ( d ( -g ` P ) e ) e. J /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) -> ( ( ( deg1 ` R ) ` ( d ( -g ` P ) e ) ) < b -> ( d ( -g ` P ) e ) e. I ) ) |
150 |
143 144 149
|
syl2anc |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( ( ( deg1 ` R ) ` ( d ( -g ` P ) e ) ) < b -> ( d ( -g ` P ) e ) e. I ) ) |
151 |
137 150
|
mpd |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( d ( -g ` P ) e ) e. I ) |
152 |
2 124
|
lidlacl |
|- ( ( ( P e. Ring /\ I e. U ) /\ ( ( d ( -g ` P ) e ) e. I /\ e e. I ) ) -> ( ( d ( -g ` P ) e ) ( +g ` P ) e ) e. I ) |
153 |
113 129 151 122 152
|
syl22anc |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> ( ( d ( -g ` P ) e ) ( +g ` P ) e ) e. I ) |
154 |
127 153
|
eqeltrrd |
|- ( ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) /\ ( e e. I /\ ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) ) ) -> d e. I ) |
155 |
154
|
rexlimdvaa |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) -> ( E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ ( ( coe1 ` d ) ` b ) = ( ( coe1 ` e ) ` b ) ) -> d e. I ) ) |
156 |
111 155
|
syl5bi |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) -> ( ( ( coe1 ` d ) ` b ) e. { c | E. e e. I ( ( ( deg1 ` R ) ` e ) <_ b /\ c = ( ( coe1 ` e ) ` b ) ) } -> d e. I ) ) |
157 |
109 156
|
mpd |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ ( d e. J /\ ( ( deg1 ` R ) ` d ) <_ b ) ) -> d e. I ) |
158 |
157
|
expr |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ d e. J ) -> ( ( ( deg1 ` R ) ` d ) <_ b -> d e. I ) ) |
159 |
74 158
|
sylbid |
|- ( ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) /\ d e. J ) -> ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) -> d e. I ) ) |
160 |
159
|
ralrimiva |
|- ( ( b e. NN0 /\ ph /\ A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) -> A. d e. J ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) -> d e. I ) ) |
161 |
160
|
3exp |
|- ( b e. NN0 -> ( ph -> ( A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) -> A. d e. J ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) -> d e. I ) ) ) ) |
162 |
161
|
a2d |
|- ( b e. NN0 -> ( ( ph -> A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) -> ( ph -> A. d e. J ( ( ( deg1 ` R ) ` d ) < ( b + 1 ) -> d e. I ) ) ) ) |
163 |
39 43 53 43 66 162
|
nn0ind |
|- ( b e. NN0 -> ( ph -> A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) ) |
164 |
|
rsp |
|- ( A. a e. J ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) -> ( a e. J -> ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) ) |
165 |
163 164
|
syl6com |
|- ( ph -> ( b e. NN0 -> ( a e. J -> ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) ) ) |
166 |
165
|
com23 |
|- ( ph -> ( a e. J -> ( b e. NN0 -> ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) ) ) |
167 |
166
|
imp |
|- ( ( ph /\ a e. J ) -> ( b e. NN0 -> ( ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) ) |
168 |
167
|
rexlimdv |
|- ( ( ph /\ a e. J ) -> ( E. b e. NN0 ( ( deg1 ` R ) ` a ) < b -> a e. I ) ) |
169 |
35 168
|
mpd |
|- ( ( ph /\ a e. J ) -> a e. I ) |
170 |
7 169
|
eqelssd |
|- ( ph -> I = J ) |