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 13 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
15 11 14 syl 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( mulGrp ` P ) e. Mnd )
16 6 ad2antrr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> X e. NN0 )
17 7 ad2antrr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> Y e. NN0 )
18 8 ad2antrr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> X <_ Y )
19 nn0sub2 
 |-  ( ( X e. NN0 /\ Y e. NN0 /\ X <_ Y ) -> ( Y - X ) e. NN0 )
20 16 17 18 19 syl3anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( Y - X ) e. NN0 )
21 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
22 eqid 
 |-  ( Base ` P ) = ( Base ` P )
23 21 1 22 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. ( Base ` P ) )
24 9 23 syl 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( var1 ` R ) e. ( Base ` P ) )
25 13 22 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
26 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
27 25 26 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ ( Y - X ) e. NN0 /\ ( var1 ` R ) e. ( Base ` P ) ) -> ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
28 15 20 24 27 syl3anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
29 simplr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> c e. I )
30 eqid 
 |-  ( .r ` P ) = ( .r ` P )
31 2 22 30 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 )
32 11 12 28 29 31 syl22anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) e. I )
33 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
34 22 2 lidlss 
 |-  ( I e. U -> I C_ ( Base ` P ) )
35 12 34 syl 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> I C_ ( Base ` P ) )
36 35 29 sseldd 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> c e. ( Base ` P ) )
37 33 1 21 13 26 deg1pwle 
 |-  ( ( R e. Ring /\ ( Y - X ) e. NN0 ) -> ( ( deg1 ` R ) ` ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ ( Y - X ) )
38 9 20 37 syl2anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( deg1 ` R ) ` ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ ( Y - X ) )
39 simpr 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( deg1 ` R ) ` c ) <_ X )
40 1 33 9 22 30 28 36 20 16 38 39 deg1mulle2 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( deg1 ` R ) ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) <_ ( ( Y - X ) + X ) )
41 17 nn0cnd 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> Y e. CC )
42 16 nn0cnd 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> X e. CC )
43 41 42 npcand 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( Y - X ) + X ) = Y )
44 40 43 breqtrd 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( deg1 ` R ) ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) <_ Y )
45 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
46 45 1 21 13 26 22 30 9 36 20 16 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 ) )
47 43 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 ) )
48 46 47 eqtr3d 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> ( ( coe1 ` c ) ` X ) = ( ( coe1 ` ( ( ( Y - X ) ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( .r ` P ) c ) ) ` Y ) )
49 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 ) ) )
50 49 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 ) )
51 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 ) ) )
52 51 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 ) )
53 52 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 ) ) )
54 50 53 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 ) ) ) )
55 54 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 ) ) )
56 32 44 48 55 syl12anc 
 |-  ( ( ( ph /\ c e. I ) /\ ( ( deg1 ` R ) ` c ) <_ X ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) )
57 eqeq1 
 |-  ( a = ( ( coe1 ` c ) ` X ) -> ( a = ( ( coe1 ` b ) ` Y ) <-> ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) )
58 57 anbi2d 
 |-  ( a = ( ( coe1 ` c ) ` X ) -> ( ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) <-> ( ( ( deg1 ` R ) ` b ) <_ Y /\ ( ( coe1 ` c ) ` X ) = ( ( coe1 ` b ) ` Y ) ) ) )
59 58 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 ) ) ) )
60 56 59 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 ) ) ) )
61 60 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 ) ) ) )
62 61 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 ) ) ) )
63 62 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 ) ) } )
64 1 2 3 33 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 ) ) } )
65 4 5 6 64 syl3anc 
 |-  ( ph -> ( ( S ` I ) ` X ) = { a | E. c e. I ( ( ( deg1 ` R ) ` c ) <_ X /\ a = ( ( coe1 ` c ) ` X ) ) } )
66 1 2 3 33 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 ) ) } )
67 4 5 7 66 syl3anc 
 |-  ( ph -> ( ( S ` I ) ` Y ) = { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ Y /\ a = ( ( coe1 ` b ) ` Y ) ) } )
68 63 65 67 3sstr4d 
 |-  ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` I ) ` Y ) )