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

Theorem mpfrcl 19617
 Description: Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.)
Hypothesis
Ref Expression
mpfrcl.q evalSub
Assertion
Ref Expression
mpfrcl SubRing

Proof of Theorem mpfrcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ne0i 3549 . . 3 evalSub evalSub
2 mpfrcl.q . . 3 evalSub
31, 2eleq2s 2458 . 2 evalSub
4 rneq 5007 . . . 4 evalSub evalSub
5 rn0 5039 . . . 4
64, 5syl6eq 2414 . . 3 evalSub evalSub
76necon3i 2568 . 2 evalSub evalSub
8 fveq1 5631 . . . . . . 7 evalSub evalSub
9 fv01 5666 . . . . . . 7
108, 9syl6eq 2414 . . . . . 6 evalSub evalSub
1110necon3i 2568 . . . . 5 evalSub evalSub
12 reldmevls 19616 . . . . . . . 8 evalSub
1312ovprc1 6009 . . . . . . 7 evalSub
1413necon1ai 2571 . . . . . 6 evalSub
15 n0 3552 . . . . . . 7 evalSub evalSub
16 df-evls 16311 . . . . . . . . . 10 evalSub SubRing mPoly s RingHom s algSc mVar s
1716elmpt2cl2 6190 . . . . . . . . 9 evalSub
1817a1d 22 . . . . . . . 8 evalSub
1918exlimiv 1639 . . . . . . 7 evalSub
2015, 19sylbi 187 . . . . . 6 evalSub
2114, 20jcai 522 . . . . 5 evalSub
2211, 21syl 15 . . . 4 evalSub
23 fvex 5646 . . . . . . . . . . . . . 14
24 nfcv 2502 . . . . . . . . . . . . . . 15 SubRing
25 nfcsb1v 3199 . . . . . . . . . . . . . . 15 mPoly s RingHom s algSc mVar s
2624, 25nfmpt 4210 . . . . . . . . . . . . . 14 SubRing mPoly s RingHom s algSc mVar s
27 csbeq1a 3175 . . . . . . . . . . . . . . 15 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mVar s
2827mpteq2dv 4209 . . . . . . . . . . . . . 14 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mVar s
2923, 26, 28csbief 3208 . . . . . . . . . . . . 13 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mVar s
30 fveq2 5632 . . . . . . . . . . . . . . 15 SubRing SubRing
3130adantl 452 . . . . . . . . . . . . . 14 SubRing SubRing
32 fveq2 5632 . . . . . . . . . . . . . . . . 17
3332adantl 452 . . . . . . . . . . . . . . . 16
3433csbeq1d 3173 . . . . . . . . . . . . . . 15 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mVar s
35 id 19 . . . . . . . . . . . . . . . . . . 19
36 oveq1 5988 . . . . . . . . . . . . . . . . . . 19 s s
3735, 36oveqan12d 6000 . . . . . . . . . . . . . . . . . 18 mPoly s mPoly s
3837csbeq1d 3173 . . . . . . . . . . . . . . . . 17 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mVar s
39 id 19 . . . . . . . . . . . . . . . . . . . . 21
40 oveq2 5989 . . . . . . . . . . . . . . . . . . . . 21
4139, 40oveqan12rd 6001 . . . . . . . . . . . . . . . . . . . 20 s s
4241oveq2d 5997 . . . . . . . . . . . . . . . . . . 19 RingHom s RingHom s
4340adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23
4443xpeq1d 4815 . . . . . . . . . . . . . . . . . . . . . 22
4544mpteq2dv 4209 . . . . . . . . . . . . . . . . . . . . 21
4645eqeq2d 2377 . . . . . . . . . . . . . . . . . . . 20 algSc algSc
4735, 36oveqan12d 6000 . . . . . . . . . . . . . . . . . . . . . 22 mVar s mVar s
4847coeq2d 4949 . . . . . . . . . . . . . . . . . . . . 21 mVar s mVar s
49 simpl 443 . . . . . . . . . . . . . . . . . . . . . 22
50 eqidd 2367 . . . . . . . . . . . . . . . . . . . . . . 23
5143, 50mpteq12dv 4200 . . . . . . . . . . . . . . . . . . . . . 22
5249, 51mpteq12dv 4200 . . . . . . . . . . . . . . . . . . . . 21
5348, 52eqeq12d 2380 . . . . . . . . . . . . . . . . . . . 20 mVar s mVar s
5446, 53anbi12d 691 . . . . . . . . . . . . . . . . . . 19 algSc mVar s algSc mVar s
5542, 54riotaeqbidv 6449 . . . . . . . . . . . . . . . . . 18 RingHom s algSc mVar s RingHom s algSc mVar s
5655csbeq2dv 3192 . . . . . . . . . . . . . . . . 17 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mVar s
5738, 56eqtrd 2398 . . . . . . . . . . . . . . . 16 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mVar s
5857csbeq2dv 3192 . . . . . . . . . . . . . . 15 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mVar s
5934, 58eqtrd 2398 . . . . . . . . . . . . . 14 mPoly s RingHom s algSc mVar s mPoly s RingHom s algSc mVar s
6031, 59mpteq12dv 4200 . . . . . . . . . . . . 13 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mVar s
6129, 60syl5eq 2410 . . . . . . . . . . . 12 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mVar s
62 fvex 5646 . . . . . . . . . . . . 13 SubRing
6362mptex 5866 . . . . . . . . . . . 12 SubRing mPoly s RingHom s algSc mVar s
6461, 16, 63ovmpt2a 6104 . . . . . . . . . . 11 evalSub SubRing mPoly s RingHom s algSc mVar s
6564dmeqd 4984 . . . . . . . . . 10 evalSub SubRing mPoly s RingHom s algSc mVar s
66 eqid 2366 . . . . . . . . . . . 12 SubRing mPoly s RingHom s algSc mVar s SubRing mPoly s RingHom s algSc mVar s
6766dmmptss 5272 . . . . . . . . . . 11 SubRing mPoly s RingHom s algSc mVar s SubRing
6867a1i 10 . . . . . . . . . 10 SubRing mPoly s RingHom s algSc mVar s SubRing
6965, 68eqsstrd 3298 . . . . . . . . 9 evalSub SubRing
7069sseld 3265 . . . . . . . 8 evalSub SubRing
7170con3d 125 . . . . . . 7 SubRing evalSub
72 ndmfv 5659 . . . . . . 7 evalSub evalSub
7371, 72syl6 29 . . . . . 6 SubRing evalSub
7473necon1ad 2596 . . . . 5 evalSub SubRing
7574com12 27 . . . 4 evalSub SubRing
7622, 75jcai 522 . . 3 evalSub SubRing
77 df-3an 937 . . 3 SubRing SubRing
7876, 77sylibr 203 . 2 evalSub SubRing
793, 7, 783syl 18 1 SubRing
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 358   w3a 935  wex 1546   wceq 1647   wcel 1715   wne 2529  cvv 2873  csb 3167   wss 3238  c0 3543  csn 3729   cmpt 4179   cxp 4790   cdm 4792   crn 4793   ccom 4796  cfv 5358  (class class class)co 5981  crio 6439   cmap 6915  cbs 13356   ↾s cress 13357   s cpws 13557  ccrg 15548   RingHom crh 15704  SubRingcsubrg 15751  algSccascl 16262   mVar cmvr 16298   mPoly cmpl 16299   evalSub ces 16300 This theorem is referenced by:  mpff  19640  mpfaddcl  19641  mpfmulcl  19642  mpfind  19643  pf1rcl  19647  mpfpf1  19649 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-rep 4233  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-reu 2635  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-riota 6446  df-evls 16311
 Copyright terms: Public domain W3C validator