Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hbtlem6 Unicode version

Theorem hbtlem6 26481
 Description: There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015.)
Hypotheses
Ref Expression
hbtlem.p Poly1
hbtlem.u LIdeal
hbtlem.s ldgIdlSeq
hbtlem6.n RSpan
hbtlem6.r LNoeR
hbtlem6.i
hbtlem6.x
Assertion
Ref Expression
hbtlem6
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem hbtlem6
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hbtlem6.r . . 3 LNoeR
2 lnrrng 26464 . . . . 5 LNoeR
31, 2syl 15 . . . 4
4 hbtlem6.i . . . 4
5 hbtlem6.x . . . 4
6 hbtlem.p . . . . 5 Poly1
7 hbtlem.u . . . . 5 LIdeal
8 hbtlem.s . . . . 5 ldgIdlSeq
9 eqid 2316 . . . . 5 LIdeal LIdeal
106, 7, 8, 9hbtlem2 26476 . . . 4 LIdeal
113, 4, 5, 10syl3anc 1182 . . 3 LIdeal
12 eqid 2316 . . . 4 RSpan RSpan
139, 12lnr2i 26468 . . 3 LNoeR LIdeal RSpan
141, 11, 13syl2anc 642 . 2 RSpan
15 elfpw 7202 . . . . 5
16 fvex 5577 . . . . . . . . 9 coe1
17 eqid 2316 . . . . . . . . 9 deg1 coe1 deg1 coe1
1816, 17fnmpti 5409 . . . . . . . 8 deg1 coe1 deg1
1918a1i 10 . . . . . . 7 deg1 coe1 deg1
20 simprl 732 . . . . . . . 8
21 eqid 2316 . . . . . . . . . . . 12 deg1 deg1
226, 7, 8, 21hbtlem1 26475 . . . . . . . . . . 11 LNoeR deg1 coe1
231, 4, 5, 22syl3anc 1182 . . . . . . . . . 10 deg1 coe1
2417rnmpt 4962 . . . . . . . . . . 11 deg1 coe1 deg1 coe1
25 fveq2 5563 . . . . . . . . . . . . . 14 deg1 deg1
2625breq1d 4070 . . . . . . . . . . . . 13 deg1 deg1
2726rexrab 2963 . . . . . . . . . . . 12 deg1 coe1 deg1 coe1
2827abbii 2428 . . . . . . . . . . 11 deg1 coe1 deg1 coe1
2924, 28eqtri 2336 . . . . . . . . . 10 deg1 coe1 deg1 coe1
3023, 29syl6eqr 2366 . . . . . . . . 9 deg1 coe1
3130adantr 451 . . . . . . . 8 deg1 coe1
3220, 31sseqtrd 3248 . . . . . . 7 deg1 coe1
33 simprr 733 . . . . . . 7
34 fipreima 7206 . . . . . . 7 deg1 coe1 deg1 deg1 coe1 deg1 deg1 coe1
3519, 32, 33, 34syl3anc 1182 . . . . . 6 deg1 deg1 coe1
36 elfpw 7202 . . . . . . . . . 10 deg1 deg1
37 ssrab2 3292 . . . . . . . . . . . . . . . . 17 deg1
38 sstr2 3220 . . . . . . . . . . . . . . . . 17 deg1 deg1
3937, 38mpi 16 . . . . . . . . . . . . . . . 16 deg1
4039adantl 452 . . . . . . . . . . . . . . 15 deg1
41 vex 2825 . . . . . . . . . . . . . . . 16
4241elpw 3665 . . . . . . . . . . . . . . 15
4340, 42sylibr 203 . . . . . . . . . . . . . 14 deg1
4443adantrr 697 . . . . . . . . . . . . 13 deg1
45 simprr 733 . . . . . . . . . . . . 13 deg1
46 elin 3392 . . . . . . . . . . . . 13
4744, 45, 46sylanbrc 645 . . . . . . . . . . . 12 deg1
483adantr 451 . . . . . . . . . . . . 13 deg1
496ply1rng 16375 . . . . . . . . . . . . . . . . 17
503, 49syl 15 . . . . . . . . . . . . . . . 16
5150adantr 451 . . . . . . . . . . . . . . 15 deg1
52 simprl 732 . . . . . . . . . . . . . . . . 17 deg1 deg1
5352, 37syl6ss 3225 . . . . . . . . . . . . . . . 16 deg1
54 eqid 2316 . . . . . . . . . . . . . . . . . . 19
5554, 7lidlss 16010 . . . . . . . . . . . . . . . . . 18
564, 55syl 15 . . . . . . . . . . . . . . . . 17
5756adantr 451 . . . . . . . . . . . . . . . 16 deg1
5853, 57sstrd 3223 . . . . . . . . . . . . . . 15 deg1
59 hbtlem6.n . . . . . . . . . . . . . . . 16 RSpan
6059, 54, 7rspcl 16023 . . . . . . . . . . . . . . 15
6151, 58, 60syl2anc 642 . . . . . . . . . . . . . 14 deg1
625adantr 451 . . . . . . . . . . . . . 14 deg1
636, 7, 8, 9hbtlem2 26476 . . . . . . . . . . . . . 14 LIdeal
6448, 61, 62, 63syl3anc 1182 . . . . . . . . . . . . 13 deg1 LIdeal
65 df-ima 4739 . . . . . . . . . . . . . . 15 deg1 coe1 deg1 coe1
6659, 54rspssid 16024 . . . . . . . . . . . . . . . . . . . . 21
6751, 58, 66syl2anc 642 . . . . . . . . . . . . . . . . . . . 20 deg1
68 ssrab 3285 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1
6968simprbi 450 . . . . . . . . . . . . . . . . . . . . 21 deg1 deg1
7069ad2antrl 708 . . . . . . . . . . . . . . . . . . . 20 deg1 deg1
71 ssrab 3285 . . . . . . . . . . . . . . . . . . . 20 deg1 deg1
7267, 70, 71sylanbrc 645 . . . . . . . . . . . . . . . . . . 19 deg1 deg1
73 resmpt 5037 . . . . . . . . . . . . . . . . . . 19 deg1 deg1 coe1 coe1
7472, 73syl 15 . . . . . . . . . . . . . . . . . 18 deg1 deg1 coe1 coe1
75 resmpt 5037 . . . . . . . . . . . . . . . . . . 19 deg1 deg1 coe1 coe1
7675ad2antrl 708 . . . . . . . . . . . . . . . . . 18 deg1 deg1 coe1 coe1
7774, 76eqtr4d 2351 . . . . . . . . . . . . . . . . 17 deg1 deg1 coe1 deg1 coe1
78 resss 5016 . . . . . . . . . . . . . . . . . 18 deg1 coe1 deg1 coe1
7978a1i 10 . . . . . . . . . . . . . . . . 17 deg1 deg1 coe1 deg1 coe1
8077, 79eqsstr3d 3247 . . . . . . . . . . . . . . . 16 deg1 deg1 coe1 deg1 coe1
81 rnss 4944 . . . . . . . . . . . . . . . 16 deg1 coe1 deg1 coe1 deg1 coe1 deg1 coe1
8280, 81syl 15 . . . . . . . . . . . . . . 15 deg1 deg1 coe1 deg1 coe1
8365, 82syl5eqss 3256 . . . . . . . . . . . . . 14 deg1 deg1 coe1 deg1 coe1
846, 7, 8, 21hbtlem1 26475 . . . . . . . . . . . . . . . 16 deg1 coe1
8548, 61, 62, 84syl3anc 1182 . . . . . . . . . . . . . . 15 deg1 deg1 coe1
86 eqid 2316 . . . . . . . . . . . . . . . . 17 deg1 coe1 deg1 coe1
8786rnmpt 4962 . . . . . . . . . . . . . . . 16 deg1 coe1 deg1 coe1
8826rexrab 2963 . . . . . . . . . . . . . . . . 17 deg1 coe1 deg1 coe1
8988abbii 2428 . . . . . . . . . . . . . . . 16 deg1 coe1 deg1 coe1
9087, 89eqtri 2336 . . . . . . . . . . . . . . 15 deg1 coe1 deg1 coe1
9185, 90syl6eqr 2366 . . . . . . . . . . . . . 14 deg1 deg1 coe1
9283, 91sseqtr4d 3249 . . . . . . . . . . . . 13 deg1 deg1 coe1
9312, 9rspssp 16027 . . . . . . . . . . . . 13 LIdeal deg1 coe1 RSpan deg1 coe1
9448, 64, 92, 93syl3anc 1182 . . . . . . . . . . . 12 deg1 RSpan deg1 coe1
9547, 94jca 518 . . . . . . . . . . 11 deg1 RSpan deg1 coe1
96 fveq2 5563 . . . . . . . . . . . . 13 deg1 coe1 RSpan deg1 coe1 RSpan
9796sseq1d 3239 . . . . . . . . . . . 12 deg1 coe1 RSpan deg1 coe1 RSpan
9897anbi2d 684 . . . . . . . . . . 11 deg1 coe1 RSpan deg1 coe1 RSpan
9995, 98syl5ibcom 211 . . . . . . . . . 10 deg1 deg1 coe1 RSpan
10036, 99sylan2b 461 . . . . . . . . 9 deg1 deg1 coe1 RSpan
101100expimpd 586 . . . . . . . 8 deg1 deg1 coe1 RSpan
102101adantr 451 . . . . . . 7 deg1 deg1 coe1 RSpan
103102reximdv2 2686 . . . . . 6 deg1 deg1 coe1 RSpan
10435, 103mpd 14 . . . . 5 RSpan
10515, 104sylan2b 461 . . . 4 RSpan
106 sseq1 3233 . . . . 5 RSpan RSpan
107106rexbidv 2598 . . . 4 RSpan RSpan
108105, 107syl5ibrcom 213 . . 3 RSpan
109108rexlimdva 2701 . 2 RSpan
11014, 109mpd 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wceq 1633   wcel 1701  cab 2302  wral 2577  wrex 2578  crab 2581   cin 3185   wss 3186  cpw 3659   class class class wbr 4060   cmpt 4114   crn 4727   cres 4728  cima 4729   wfn 5287  cfv 5292  cfn 6906   cle 8913  cn0 10012  cbs 13195  crg 15386  LIdealclidl 15972  RSpancrsp 15973  Poly1cpl1 16301  coe1cco1 16304   deg1 cdg1 19493  LNoeRclnr 26461  ldgIdlSeqcldgis 26473 This theorem is referenced by:  hbt  26482 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859  ax-pre-sup 8860  ax-addf 8861  ax-mulf 8862 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-iin 3945  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-of 6120  df-ofr 6121  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-2o 6522  df-oadd 6525  df-er 6702  df-map 6817  df-pm 6818  df-ixp 6861  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-sup 7239  df-oi 7270  df-card 7617  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-2 9849  df-3 9850  df-4 9851  df-5 9852  df-6 9853  df-7 9854  df-8 9855  df-9 9856  df-10 9857  df-n0 10013  df-z 10072  df-dec 10172  df-uz 10278  df-fz 10830  df-fzo 10918  df-seq 11094  df-hash 11385  df-struct 13197  df-ndx 13198  df-slot 13199  df-base 13200  df-sets 13201  df-ress 13202  df-plusg 13268  df-mulr 13269  df-starv 13270  df-sca 13271  df-vsca 13272  df-tset 13274  df-ple 13275  df-ds 13277  df-unif 13278  df-0g 13453  df-gsum 13454  df-mre 13537  df-mrc 13538  df-acs 13540  df-mnd 14416  df-mhm 14464  df-submnd 14465  df-grp 14538  df-minusg 14539  df-sbg 14540  df-mulg 14541  df-subg 14667  df-ghm 14730  df-cntz 14842  df-cmn 15140  df-abl 15141  df-mgp 15375  df-rng 15389  df-cring 15390  df-ur 15391  df-subrg 15592  df-lmod 15678  df-lss 15739  df-lsp 15778  df-sra 15974  df-rgmod 15975  df-lidl 15976  df-rsp 15977  df-ascl 16104  df-psr 16147  df-mvr 16148  df-mpl 16149  df-opsr 16155  df-psr1 16306  df-vr1 16307  df-ply1 16308  df-coe1 16311  df-cnfld 16433  df-mdeg 19494  df-deg1 19495  df-lfig 26314  df-lnm 26322  df-lnr 26462  df-ldgis 26474
 Copyright terms: Public domain W3C validator