Metamath Proof Explorer

Theorem hbtlem5

Description: The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses hbtlem.p 
|- P = ( Poly1 ` R )
hbtlem.u 
|- U = ( LIdeal ` P )
hbtlem.s 
|- S = ( ldgIdlSeq ` R )
hbtlem3.r 
|- ( ph -> R e. Ring )
hbtlem3.i 
|- ( ph -> I e. U )
hbtlem3.j 
|- ( ph -> J e. U )
hbtlem3.ij 
|- ( ph -> I C_ J )
hbtlem5.e 
|- ( ph -> A. x e. NN0 ( ( S ` J ) ` x ) C_ ( ( S ` I ) ` x ) )
Assertion hbtlem5 
|- ( ph -> I = J )

Proof

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