Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  evlsval Unicode version

Theorem evlsval 19507
 Description: Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015.)
Hypotheses
Ref Expression
evlsval.q evalSub
evlsval.w mPoly
evlsval.v mVar
evlsval.u s
evlsval.t s
evlsval.b
evlsval.a algSc
evlsval.x
evlsval.y
Assertion
Ref Expression
evlsval SubRing RingHom
Distinct variable groups:   ,,,   ,,   ,,,   ,   ,
Allowed substitution hints:   (,,)   (,,)   (,,)   ()   (,)   (,,)   (,,)   (,)   (,,)   (,,)

Proof of Theorem evlsval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evlsval.q . . . 4 evalSub
2 fveq2 5608 . . . . . . . . 9
32adantl 452 . . . . . . . 8
43csbeq1d 3163 . . . . . . 7 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mVar s
5 fvex 5622 . . . . . . . . 9
65a1i 10 . . . . . . . 8
7 simplr 731 . . . . . . . . . 10
87fveq2d 5612 . . . . . . . . 9 SubRing SubRing
9 simpll 730 . . . . . . . . . . . 12
10 oveq1 5952 . . . . . . . . . . . . 13 s s
1110ad2antlr 707 . . . . . . . . . . . 12 s s
129, 11oveq12d 5963 . . . . . . . . . . 11 mPoly s mPoly s
1312csbeq1d 3163 . . . . . . . . . 10 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mVar s
14 ovex 5970 . . . . . . . . . . . 12 mPoly s
1514a1i 10 . . . . . . . . . . 11 mPoly s
16 simprr 733 . . . . . . . . . . . . . 14 mPoly s mPoly s
17 simplr 731 . . . . . . . . . . . . . . 15 mPoly s
18 simprl 732 . . . . . . . . . . . . . . . 16 mPoly s
19 simpll 730 . . . . . . . . . . . . . . . 16 mPoly s
2018, 19oveq12d 5963 . . . . . . . . . . . . . . 15 mPoly s
2117, 20oveq12d 5963 . . . . . . . . . . . . . 14 mPoly s s s
2216, 21oveq12d 5963 . . . . . . . . . . . . 13 mPoly s RingHom s mPoly s RingHom s
2316fveq2d 5612 . . . . . . . . . . . . . . . 16 mPoly s algSc algSc mPoly s
2423coeq2d 4928 . . . . . . . . . . . . . . 15 mPoly s algSc algSc mPoly s
2520xpeq1d 4794 . . . . . . . . . . . . . . . 16 mPoly s
2625mpteq2dv 4188 . . . . . . . . . . . . . . 15 mPoly s
2724, 26eqeq12d 2372 . . . . . . . . . . . . . 14 mPoly s algSc algSc mPoly s
2817oveq1d 5960 . . . . . . . . . . . . . . . . 17 mPoly s s s
2919, 28oveq12d 5963 . . . . . . . . . . . . . . . 16 mPoly s mVar s mVar s
3029coeq2d 4928 . . . . . . . . . . . . . . 15 mPoly s mVar s mVar s
31 eqidd 2359 . . . . . . . . . . . . . . . . 17 mPoly s
3220, 31mpteq12dv 4179 . . . . . . . . . . . . . . . 16 mPoly s
3319, 32mpteq12dv 4179 . . . . . . . . . . . . . . 15 mPoly s
3430, 33eqeq12d 2372 . . . . . . . . . . . . . 14 mPoly s mVar s mVar s
3527, 34anbi12d 691 . . . . . . . . . . . . 13 mPoly s algSc mVar s algSc mPoly s mVar s
3622, 35riotaeqbidv 6394 . . . . . . . . . . . 12 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mPoly s mVar s
3736anassrs 629 . . . . . . . . . . 11 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mPoly s mVar s
3815, 37csbied 3199 . . . . . . . . . 10 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mPoly s mVar s
3913, 38eqtrd 2390 . . . . . . . . 9 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mPoly s mVar s
408, 39mpteq12dv 4179 . . . . . . . 8 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mPoly s mVar s
416, 40csbied 3199 . . . . . . 7 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mPoly s mVar s
424, 41eqtrd 2390 . . . . . 6 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mPoly s mVar s
43 df-evls 16200 . . . . . 6 evalSub SubRing mPoly s RingHom s algSc mVar s
44 fvex 5622 . . . . . . 7 SubRing
4544mptex 5832 . . . . . 6 SubRing mPoly s RingHom s algSc mPoly s mVar s
4642, 43, 45ovmpt2a 6065 . . . . 5 evalSub SubRing mPoly s RingHom s algSc mPoly s mVar s
4746fveq1d 5610 . . . 4 evalSub SubRing mPoly s RingHom s algSc mPoly s mVar s
481, 47syl5eq 2402 . . 3 SubRing mPoly s RingHom s algSc mPoly s mVar s
49483adant3 975 . 2 SubRing SubRing mPoly s RingHom s algSc mPoly s mVar s
50 oveq2 5953 . . . . . . . 8 s s
5150oveq2d 5961 . . . . . . 7 mPoly s mPoly s
5251oveq1d 5960 . . . . . 6 mPoly s RingHom s mPoly s RingHom s
5351fveq2d 5612 . . . . . . . . 9 algSc mPoly s algSc mPoly s
5453coeq2d 4928 . . . . . . . 8 algSc mPoly s algSc mPoly s
55 mpteq1 4181 . . . . . . . 8
5654, 55eqeq12d 2372 . . . . . . 7 algSc mPoly s algSc mPoly s
5750oveq2d 5961 . . . . . . . . 9 mVar s mVar s
5857coeq2d 4928 . . . . . . . 8 mVar s mVar s
5958eqeq1d 2366 . . . . . . 7 mVar s mVar s
6056, 59anbi12d 691 . . . . . 6 algSc mPoly s mVar s algSc mPoly s mVar s
6152, 60riotaeqbidv 6394 . . . . 5 mPoly s RingHom s algSc mPoly s mVar s mPoly s RingHom s algSc mPoly s mVar s
62 eqid 2358 . . . . 5 SubRing mPoly s RingHom s algSc mPoly s mVar s SubRing mPoly s RingHom s algSc mPoly s mVar s
63 riotaex 6395 . . . . 5 mPoly s RingHom s algSc mPoly s mVar s
6461, 62, 63fvmpt 5685 . . . 4 SubRing SubRing mPoly s RingHom s algSc mPoly s mVar s mPoly s RingHom s algSc mPoly s mVar s
65 evlsval.w . . . . . . . . 9 mPoly
66 evlsval.u . . . . . . . . . 10 s
6766oveq2i 5956 . . . . . . . . 9 mPoly mPoly s
6865, 67eqtri 2378 . . . . . . . 8 mPoly s
69 evlsval.t . . . . . . . . 9 s
70 evlsval.b . . . . . . . . . . 11
7170oveq1i 5955 . . . . . . . . . 10
7271oveq2i 5956 . . . . . . . . 9 s s
7369, 72eqtri 2378 . . . . . . . 8 s
7468, 73oveq12i 5957 . . . . . . 7 RingHom mPoly s RingHom s
7574a1i 10 . . . . . 6 RingHom mPoly s RingHom s
76 evlsval.a . . . . . . . . . . 11 algSc
7768fveq2i 5611 . . . . . . . . . . 11 algSc algSc mPoly s
7876, 77eqtri 2378 . . . . . . . . . 10 algSc mPoly s
7978coeq2i 4926 . . . . . . . . 9 algSc mPoly s
80 evlsval.x . . . . . . . . . 10
8171xpeq1i 4791 . . . . . . . . . . 11
8281mpteq2i 4184 . . . . . . . . . 10
8380, 82eqtri 2378 . . . . . . . . 9
8479, 83eqeq12i 2371 . . . . . . . 8 algSc mPoly s
85 evlsval.v . . . . . . . . . . 11 mVar
8666oveq2i 5956 . . . . . . . . . . 11 mVar mVar s
8785, 86eqtri 2378 . . . . . . . . . 10 mVar s
8887coeq2i 4926 . . . . . . . . 9 mVar s
89 evlsval.y . . . . . . . . . 10
90 eqid 2358 . . . . . . . . . . . 12
9171, 90mpteq12i 4185 . . . . . . . . . . 11
9291mpteq2i 4184 . . . . . . . . . 10
9389, 92eqtri 2378 . . . . . . . . 9
9488, 93eqeq12i 2371 . . . . . . . 8 mVar s
9584, 94anbi12i 678 . . . . . . 7 algSc mPoly s mVar s
9695a1i 10 . . . . . 6 algSc mPoly s mVar s
9775, 96riotaeqbidv 6394 . . . . 5 RingHom mPoly s RingHom s algSc mPoly s mVar s
9897trud 1323 . . . 4 RingHom mPoly s RingHom s algSc mPoly s mVar s
9964, 98syl6eqr 2408 . . 3 SubRing SubRing mPoly s RingHom s algSc mPoly s mVar s RingHom
100993ad2ant3 978 . 2 SubRing SubRing mPoly s RingHom s algSc mPoly s mVar s RingHom
10149, 100eqtrd 2390 1 SubRing RingHom
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wtru 1316   wceq 1642   wcel 1710  cvv 2864  csb 3157  csn 3716   cmpt 4158   cxp 4769   ccom 4775  cfv 5337  (class class class)co 5945  crio 6384   cmap 6860  cbs 13245   ↾s cress 13246   s cpws 13446  ccrg 15437   RingHom crh 15593  SubRingcsubrg 15640  algSccascl 16151   mVar cmvr 16187   mPoly cmpl 16188   evalSub ces 16189 This theorem is referenced by:  evlsval2  19508 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pr 4295 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-riota 6391  df-evls 16200
 Copyright terms: Public domain W3C validator