Metamath Proof Explorer

Theorem hbtlem4

Description: The leading ideal function goes to increasing sequences. (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 )
hbtlem4.r 
|- ( ph -> R e. Ring )
hbtlem4.i 
|- ( ph -> I e. U )
hbtlem4.x 
|- ( ph -> X e. NN0 )
hbtlem4.y 
|- ( ph -> Y e. NN0 )
hbtlem4.xy 
|- ( ph -> X <_ Y )
Assertion hbtlem4 
|- ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` I ) ` Y ) )

Proof

Step Hyp Ref Expression
1 hbtlem.p 
 |-  P = ( Poly1 ` R )
2 hbtlem.u 
 |-  U = ( LIdeal ` P )
3 hbtlem.s 
 |-  S = ( ldgIdlSeq ` R )
4 hbtlem4.r 
 |-  ( ph -> R e. Ring )
5 hbtlem4.i 
 |-  ( ph -> I e. U )
6 hbtlem4.x 
 |-  ( ph -> X e. NN0 )
7 hbtlem4.y 
 |-  ( ph -> Y e. NN0 )
8 hbtlem4.xy 
 |-  ( ph -> X <_ Y )
9 4 ad2antrr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> R e. Ring )
10 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
11 9 10 syl 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> P e. Ring )
12 5 ad2antrr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> I e. U )
13 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
14 eqid 
 |-  ( Base ` P ) = ( Base ` P )
15 13 14 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
16 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
17 13 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
18 11 17 syl 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( mulGrp ` P ) e. Mnd )
19 6 ad2antrr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> X e. NN0 )
20 7 ad2antrr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> Y e. NN0 )
21 8 ad2antrr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> X <_ Y )
22 nn0sub2 
 |-  ( ( X e. NN0 /\ Y e. NN0 /\ X <_ Y ) -> ( Y - X ) e. NN0 )
23 19 20 21 22 syl3anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( Y - X ) e. NN0 )
24 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
25 24 1 14 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. ( Base ` P ) )
26 9 25 syl 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( var1 ` R ) e. ( Base ` P ) )
27 15 16 18 23 26 mulgnn0cld 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
28 simplr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> c e. I )
29 eqid 
 |-  ( .r ` P ) = ( .r ` P )
30 2 14 29 lidlmcl 
 |-  ( ( ( P e. Ring /\ I e. U ) /\ ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) /\ c e. I ) ) -> ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) e. I )
31 11 12 27 28 30 syl22anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) e. I )
32 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
33 14 2 lidlss 
 |-  ( I e. U -> I C_ ( Base ` P ) )
34 12 33 syl 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> I C_ ( Base ` P ) )
35 34 28 sseldd 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> c e. ( Base ` P ) )
36 32 1 24 13 16 deg1pwle 
 |-  ( ( R e. Ring /\ ( Y - X ) e. NN0 ) -> ( ( deg1 ` R ) ` ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ ( Y - X ) )
37 9 23 36 syl2anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( deg1 ` R ) ` ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ ( Y - X ) )
38 simpr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( deg1 ` R ) ` c ) <_ X )
39 1 32 9 14 29 27 35 23 19 37 38 deg1mulle2 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( deg1 ` R ) ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) <_ ( ( Y - X ) + X ) )
40 20 nn0cnd 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> Y e. CC )
41 19 nn0cnd 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> X e. CC )
42 40 41 npcand 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( Y - X ) + X ) = Y )
43 39 42 breqtrd 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( deg1 ` R ) ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) <_ Y )
44 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
45 44 1 24 13 16 14 29 9 35 23 19 coe1pwmulfv 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` ( ( Y - X ) + X ) ) = ( ( coe1 ` c ) ` X ) )
46 42 fveq2d 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` ( ( Y - X ) + X ) ) = ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` Y ) )
47 45 46 eqtr3d 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( coe1 ` c ) ` X ) = ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` Y ) )
48 fveq2 
 |-  ( b = ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) -> ( ( deg1 ` R ) ` b ) = ( ( deg1 ` R ) ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) )
49 48 breq1d 
 |-  ( b = ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) -> ( ( ( deg1 ` R ) ` b ) <_ Y <-> ( ( deg1 ` R ) ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) <_ Y ) )
50 fveq2 
 |-  ( b = ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) -> ( coe1 ` b ) = ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) )
51 50 fveq1d 
 |-  ( b = ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) -> ( ( coe1 ` b ) ` Y ) = ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` Y ) )
52 51 eqeq2d 
 |-  ( b = ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) -> ( ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) <-> ( ( coe1 ` c ) ` X ) = ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` Y ) ) )
53 49 52 anbi12d 
 |-  ( b = ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) -> ( ( ( ( deg1 ` R ) ` b ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) <-> ( ( ( deg1 ` R ) ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` Y ) ) ) )
54 53 rspcev 
 |-  ( ( ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) e. I /\ ( ( ( deg1 ` R ) ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` Y ) ) ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) )
55 31 43 47 54 syl12anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) )
56 eqeq1 
 |-  ( a = ( ( coe1 ` c ) ` X ) -> ( a = ( ( coe1 ` b ) ` Y ) <-> ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) )
57 56 anbi2d 
 |-  ( a = ( ( coe1 ` c ) ` X ) -> ( ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) <-> ( ( ( deg1 ` R ) ` b ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) ) )
58 57 rexbidv 
 |-  ( a = ( ( coe1 ` c ) ` X ) -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) <-> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) ) )
59 55 58 syl5ibrcom 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( a = ( ( coe1 ` c ) ` X ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) ) )
60 59 expimpd 
 |-  ( ( ph /\ c e. I ) -> ( ( ( ( deg1 ` R ) ` c ) <_ X /\ a = ( ( coe1 ` c ) ` X ) ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) ) )
61 60 rexlimdva 
 |-  ( ph -> ( E. c e. I ( ( ( deg1 ` R ) ` c ) <_ X /\ a = ( ( coe1 ` c ) ` X ) ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) ) )
62 61 ss2abdv 
 |-  ( ph -> { a | E. c e. I ( ( ( deg1 ` R ) ` c ) <_ X /\ a = ( ( coe1 ` c ) ` X ) ) } C_ { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) } )
63 1 2 3 32 hbtlem1 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = { a | E. c e. I ( ( ( deg1 ` R ) ` c ) <_ X /\ a = ( ( coe1 ` c ) ` X ) ) } )
64 4 5 6 63 syl3anc 
 |-  ( ph -> ( ( S ` I ) ` X ) = { a | E. c e. I ( ( ( deg1 ` R ) ` c ) <_ X /\ a = ( ( coe1 ` c ) ` X ) ) } )
65 1 2 3 32 hbtlem1 
 |-  ( ( R e. Ring /\ I e. U /\ Y e. NN0 ) -> ( ( S ` I ) ` Y ) = { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) } )
66 4 5 7 65 syl3anc 
 |-  ( ph -> ( ( S ` I ) ` Y ) = { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) } )
67 62 64 66 3sstr4d 
 |-  ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` I ) ` Y ) )