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

Theorem fveq1d 5883
Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
fveq1d.1  |-  ( ph  ->  F  =  G )
Assertion
Ref Expression
fveq1d  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )

Proof of Theorem fveq1d
StepHypRef Expression
1 fveq1d.1 . 2  |-  ( ph  ->  F  =  G )
2 fveq1 5880 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2syl 17 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609
This theorem is referenced by:  fveq12d  5887  funssfv  5896  csbfv12  5916  csbfv2g  5917  fvmptd  5970  fvmpt2d  5975  mpteqb  5980  fvmptt  5981  fnmptfvd  6000  fmptco  6071  fvunsn  6111  fvsng  6113  fsnunfv  6119  f1ocnvfv1  6190  f1ocnvfv2  6191  fcof1  6200  fcofo  6201  csbov123  6339  elovmpt3rab1  6541  ofval  6554  offval2f  6557  offval2  6562  ofrfval2  6563  caofinvl  6572  curry1val  6900  curry2val  6904  fnwelem  6922  fvmpt2curryd  7026  rdg0g  7153  oav  7221  omv  7222  oev  7224  resixpfo  7568  pw2f1olem  7682  mapxpen  7744  xpmapenlem  7745  ordtypelem6  8038  ordtypelem7  8039  unwdomg  8099  cantnffval  8167  cantnfval  8172  cantnfres  8181  cantnfp1lem3  8184  fseqenlem1  8453  fseqenlem2  8454  iunfictbso  8543  dfac12lem1  8571  dfac12lem2  8572  dfac12r  8574  ackbij2lem3  8669  ituni0  8846  itunisuc  8847  itunitc1  8848  ituniiun  8850  hsmexlem2  8855  hsmexlem4  8857  iundom2g  8963  konigthlem  8991  konigth  8992  fpwwe2lem6  9059  fpwwe2lem9  9062  rpnnen1lem3  11292  rpnnen1lem5  11294  fseq1p1m1  11866  seqp1  12225  seqf1olem2  12250  seqf1o  12251  seqid  12255  seqz  12258  seqof  12267  seqof2  12268  bcval5  12500  bcn2  12501  hashf1lem1  12613  seqcoll  12621  s1fv  12733  ccat2s1fvw  12756  swrdfv  12765  swrdswrd  12801  splfv1  12847  revfv  12853  cshwidxmod  12890  ccat2s1fvwALT  13009  relexpsucnnr  13067  shftcan1  13125  shftcan2  13126  climshft2  13624  isercoll2  13710  sumeq2w  13736  sumeq2ii  13737  summo  13761  fsum  13764  fsumss  13769  fsumcvg2  13771  isumsplit  13876  prodeq2w  13944  prodeq2ii  13945  prodmo  13968  fprod  13973  fprodss  13980  bpolylem  14079  rpnnen2lem1  14245  rpnnen2  14256  ruclem4  14264  sadfval  14400  smufval  14425  odzval  14696  1arithlem2  14822  vdwpc  14884  vdwlem6  14890  ramval  14914  ramvalOLD  14915  fvsetsid  15102  setsid  15118  setsnid  15119  prdsval  15303  prdsplusgfval  15322  prdsmulrfval  15324  pwsvscaval  15343  imasval  15359  xpsc0  15408  xpsc1  15409  mrisval  15478  comfffval  15545  sectffval  15597  invinv  15617  oppcsect  15625  invisoinvl  15637  brcic  15645  brssc  15661  issubc  15682  isfunc  15711  funcoppc  15722  idfuval  15723  idfu2  15725  idfu1  15727  idfucl  15728  cofuval  15729  cofu1  15731  cofu2  15733  cofuval2  15734  cofucl  15735  cofurid  15738  resfval  15739  resfval2  15740  funcres  15743  funcpropd  15747  isfull  15757  isnat  15794  fucco  15809  homafval  15866  idafval  15894  setcmon  15924  catcisolem  15943  catciso  15944  funcestrcsetclem6  15972  funcsetcestrclem6  15987  xpcval  16004  1stf1  16019  2ndf1  16022  1stfcl  16024  2ndfcl  16025  prfval  16026  prf2fval  16028  prf1st  16031  prf2nd  16032  1st2ndprf  16033  evlf2  16045  evlf2val  16046  evlfcl  16049  curfval  16050  curfpropd  16060  uncfval  16061  uncf2  16064  curfuncf  16065  diag11  16070  diag12  16071  diag2  16072  curf2ndf  16074  hofval  16079  hofcl  16086  yon11  16091  yon12  16092  yon2  16093  yonedalem4a  16102  yonedalem4b  16103  yonedalem4c  16104  yonedalem22  16105  yonedalem3b  16106  yonedainv  16108  yoniso  16112  lubval  16172  glbval  16185  poslubdg  16337  gsumvalx  16455  gsumpropd  16457  gsumress  16461  gsumval2a  16464  prdspjmhm  16556  pwsco1mhm  16559  grpsubfval  16650  grplactval  16695  grpsubpropd  16698  grpsubpropd2  16699  mulgfval  16701  mulgpropd  16733  submmulg  16735  pwsinvg  16740  subgmulg  16773  eqgfval  16807  cntrval  16915  cntzval  16917  cntzrcl  16923  oppgsubg  16956  lactghmga  16987  symgga  16989  gsmsymgrfixlem1  17010  gsmsymgrfix  17011  gsmsymgreqlem1  17013  gsmsymgreqlem2  17014  gsmsymgreq  17015  pmtrval  17034  pmtrfv  17035  pmtrffv  17042  pmtrdifwrdellem3  17066  pmtrdifwrdel2lem1  17067  pmtrdifwrdel  17068  pmtrdifwrdel2  17069  ispgp  17170  vrgpval  17343  frgpup3lem  17353  frgpnabllem1  17435  frgpnabllem2  17436  gsumval3eu  17464  gsumval3lem2  17466  gsumval3  17467  gsumzres  17469  gsumzf1o  17472  gsumzaddlem  17480  gsumconst  17493  dmdprd  17556  dprdval  17561  dmdprdsplitlem  17596  dprd2da  17601  dpjfval  17614  dpjidcl  17617  dpjlid  17620  dpjrid  17621  dvrfval  17838  staffval  18001  srngnvl  18010  issrngd  18015  lspval  18124  islbs  18225  lbspropd  18248  lssacsex  18293  lbsacsbs  18305  sralem  18326  srasca  18330  sravsca  18331  sraip  18332  rlmval  18340  ixpsnbasval  18358  lpival  18395  rrgsupp  18441  aspval  18478  psrmulval  18536  psrvscaval  18542  psrdi  18556  psrdir  18557  mvrval  18571  mvrval2  18572  mvrf1  18575  mplsubglem  18584  mplvscaval  18598  subrgmvrf  18612  opsrle  18625  opsrbaslem  18627  subrgasclcl  18648  evlslem1  18664  evlsval  18668  evlssca  18671  evlsvar  18672  evlval  18673  evlsscasrng  18675  evlsvarsrng  18677  evlvar  18678  psr1val  18705  vr1val  18711  coe1fv  18725  subrgvr1  18780  coe1addfv  18784  coe1subfv  18785  coe1tmfv1  18793  coe1tmfv2  18794  coe1tmmul2fv  18797  coe1pwmulfv  18799  coe1sclmulfv  18802  ply1sclid  18807  ply1sclf1  18808  ply1coe1eq  18818  cply1coe0bi  18820  coe1fzgsumdlem  18821  coe1fzgsumd  18822  gsummoncoe1  18824  gsumply1eq  18825  evls1val  18835  evls1sca  18838  evl1sca  18848  evl1scad  18849  evl1var  18850  evl1vard  18851  evls1var  18852  evls1scasrng  18853  evls1varsrng  18854  evl1addd  18855  evl1subd  18856  evl1muld  18857  evl1vsd  18858  evl1expd  18859  pf1ind  18869  evl1gsumdlem  18870  evl1gsumd  18871  evl1gsumadd  18872  zrhmulg  19003  chrval  19018  chrrhm  19024  znzrhval  19039  psgndiflemA  19091  ocvval  19152  elocv  19153  cssval  19167  pjfval  19191  pjfo  19200  isobs  19205  dsmmval  19219  dsmm0cl  19225  prdsinvgd2  19227  frlmvscaval  19251  frlmphl  19261  uvcval  19265  uvcvval  19266  uvcresum  19273  mat1dimscm  19422  mat1rhmelval  19427  marepvval  19514  mdetfval  19533  mdetleib2  19535  mdet0fv0  19541  m1detdiag  19544  mdetdiaglem  19545  mdetralt  19555  mdetunilem7  19565  mdetuni0  19568  m2detleiblem1  19571  smadiadetr  19622  cramerimplem1  19630  cpmatel  19657  1elcpmat  19661  cpmatinvcl  19663  cpmatmcllem  19664  cpmatmcl  19665  mat2pmatfval  19669  m2cpm  19687  cpm2mval  19696  cpm2mvalel  19697  m2cpminvid  19699  m2cpminvid2lem  19700  m2cpminvid2  19701  m2cpmfo  19702  decpmate  19712  decpmatid  19716  decpmatmullem  19717  decpmatmulsumfsupp  19719  monmatcollpw  19725  pmatcollpw3lem  19729  pmatcollpwscmatlem1  19735  pmatcollpwscmatlem2  19736  pm2mpf1  19745  pm2mpcoe1  19746  mply1topmatval  19750  mp2pm2mplem1  19752  mp2pm2mplem3  19754  mp2pm2mplem4  19755  mp2pm2mp  19757  pm2mpghm  19762  pm2mpmhmlem1  19764  pm2mpmhmlem2  19765  chpmatfval  19776  chpmat0d  19780  chpscmatgsumbin  19790  cayleyhamilton0  19835  cayleyhamiltonALT  19837  ntrval  19973  clsval  19974  opncldf3  20024  neival  20040  neiptopreu  20071  lpfval  20076  lpval  20077  cnpval  20174  iscnp2  20177  isreg  20270  isnrm  20273  2ndcsep  20396  isnlly  20406  ptval  20507  dfac14  20555  cnmptk2  20623  pt1hmeo  20743  xkocnv  20751  fmval  20880  ufldom  20899  flimval  20900  flffval  20926  flfval  20927  cnpflf  20938  txflf  20943  fclsval  20945  fcfval  20970  flfcntr  20980  cnextval  20998  cnextfvval  21002  cnextcn  21004  cnextfres1  21005  cnextfres  21006  symgtgp  21038  tgpconcomp  21049  prdstmdd  21060  utopsnneiplem  21184  neipcfilu  21233  txmetcnp  21484  subgnm2  21564  tngngp  21584  isnlm  21600  sranlm  21609  lssnlm  21625  nmofval  21637  nmoval  21638  isphtpy  21896  pcovalg  21927  pco1  21930  clmneg  21996  clmabs  21997  nmoleub2lem3  22013  nmoleub3  22017  cphcjcl  22045  cphnm  22055  cphipcj  22061  cphassr  22073  tchnmval  22087  tchcphlem3  22091  ipcau2  22092  tchcphlem1  22093  tchcphlem2  22094  tchcph  22095  ipcau  22096  rrxnm  22234  rrxmval  22243  ovolctb  22312  voliunlem3  22373  uniioombllem2  22408  uniioombllem2OLD  22409  vitalilem4  22437  mbflimsup  22491  mbflimsupOLD  22492  itg1climres  22540  mbfi1fseqlem4  22544  mbfi1fseqlem5  22545  mbfi1fseqlem6  22546  mbfi1flimlem  22548  mbfmullem2  22550  mbfmullem  22551  itg2monolem1  22576  itg2mono  22579  itg2i1fseqle  22580  itg2i1fseq  22581  itg2addlem  22584  itg2cnlem1  22587  limcfval  22695  limcmpt2  22707  limcres  22709  cnplimc  22710  dvfval  22720  dvreslem  22732  dvres2lem  22733  dvn0  22746  dvnp1  22747  cpnfval  22754  elcpn  22756  dvaddbr  22760  dvmulbr  22761  dvcmul  22766  dvfre  22773  rolle  22810  cmvth  22811  mvth  22812  dvlip  22813  dvlipcn  22814  dvlip2  22815  c1liplem1  22816  dveq0  22820  dv11cn  22821  dvivthlem1  22828  dvivth  22830  dvne0  22831  lhop1lem  22833  lhop2  22835  lhop  22836  dvcnvrelem2  22838  dvcvx  22840  dvfsumabs  22843  ftc1lem6  22861  ftc2  22864  ftc2ditglem  22865  itgparts  22867  itgsubstlem  22868  mdegaddle  22891  mdegmullem  22895  coe1mul3  22916  uc1pval  22956  mon1pval  22958  uc1pmon1p  22968  q1pval  22970  ply1remlem  22979  ply1rem  22980  fta1glem2  22983  fta1g  22984  fta1blem  22985  ig1pval  22989  plyeq0lem  23023  coeeulem  23037  coeid2  23052  dgrle  23056  dgreq  23057  0dgrb  23059  dgrnznn  23060  coemul  23065  coe11  23066  coe1term  23072  dgrlt  23079  dgradd2  23081  dgrcolem2  23087  plymul0or  23093  plydivlem4  23108  plydiveu  23110  plyremlem  23116  plyrem  23117  fta1  23120  vieta1lem2  23123  plyexmo  23125  aareccl  23138  aannenlem1  23140  aannenlem2  23141  taylfval  23170  tayl0  23173  dvtaylp  23181  dvntaylp0  23183  taylthlem1  23184  taylthlem2  23185  ulmval  23191  ulmres  23199  ulmshftlem  23200  ulmshft  23201  ulmuni  23203  ulmcaulem  23205  ulmcau  23206  ulmss  23208  ulmdvlem1  23211  ulmdvlem3  23213  mtest  23215  mtestbdd  23216  mbfulm  23217  itgulm  23219  itgulm2  23220  pserval2  23222  pserulm  23233  psercn  23237  pserdvlem2  23239  pserdv  23240  pige3  23328  logtayl  23461  rlimcnp  23747  lgamgulmlem2  23811  lgamgulmlem5  23814  lgamgulm2  23817  lgamcvglem  23821  sqff1o  23963  muinv  23976  dchrinv  24043  sumdchr2  24052  dchr2sum  24055  lgsval4  24098  lgsmod  24103  lgsqrlem1  24123  dchrmusumlema  24185  dchrvmasumlem1  24187  dchrisum0re  24205  dchrisum0lema  24206  logsqvma2  24235  padicval  24309  istrkg2ld  24362  iscgrg  24411  midexlem  24585  israg  24590  colperpexlem2  24621  colperpexlem3  24622  opphllem  24625  midex  24627  mideu  24628  opphllem3  24639  midf  24665  ismidb  24667  lmieu  24673  lmimid  24683  iscgra  24698  isinag  24723  brcgr  24767  ecgrtg  24850  wwlkn  25246  wlkiswwlkfun  25281  wlkiswwlkinj  25282  wlkiswwlksur  25283  wlkiswwlkbij2  25285  clwwlkn  25331  vdgrfval  25459  vdgrval  25460  isrgra  25490  isrgrac  25498  rusgranumwlklem4  25516  iseupa  25529  eupath2lem3  25543  eupath2  25544  vdfrgra0  25586  grpoinvval  25789  grpodivfval  25806  gxfval  25821  gxval  25822  imsdval  26154  sspnval  26212  nmoofval  26239  nmooval  26240  bloval  26258  0oval  26265  nmlno0  26272  hmoval  26287  ajval  26339  ubth  26351  htthlem  26396  pjhval  26876  pjoc1  26913  pjoc2  26918  pjige0  27170  pjcjt2  27171  pjch  27173  pjsumi  27189  pjdsi  27191  pjds3i  27192  pjopyth  27199  pjnorm  27203  pjpyth  27204  pjnel  27205  hosval  27219  homval  27220  hodval  27221  hfsval  27222  hfmval  27223  braval  27423  kbval  27433  eigvalval  27439  leopg  27601  leoppos  27605  leoprf2  27606  leoprf  27607  elpjrn  27669  pj3cor1i  27688  strlem2  27730  hstrlem2  27738  fmptcof2  28090  resf1o  28149  fpwrelmap  28152  lmatval  28469  lmatfvlem  28471  madjusmdetlem1  28483  fmcncfil  28567  nmmulg  28602  zrhnm  28603  qqhval  28608  qqhcn  28625  rrhqima  28648  xrhval  28652  ofcfval  28749  ofcfval3  28753  brfae  28901  omsval  28945  sitgval  28984  eulerpartlemsv1  29006  eulerpartlemsf  29009  eulerpartlemgvv  29026  eulerpartlemn  29031  sseqval  29038  sseqfv1  29039  sseqfv2  29044  fibp1  29051  dstrvval  29120  ballotleme  29146  ballotlemi  29150  plymulx0  29215  plymulx  29216  signstfv  29231  signstfvneq0  29240  signstfvc  29242  signstres  29243  signstfveq0  29245  signsvvfval  29246  bnj1379  29421  subfacp1lem5  29686  kur14  29718  ptpcon  29735  cvmliftmolem1  29783  cvmliftlem5  29791  cvmliftlem7  29793  cvmliftlem15  29800  cvmlift2lem3  29807  cvmlift2lem4  29808  cvmlift2lem7  29811  cvmlift2lem9  29813  cvmlift2  29818  cvmliftphtlem  29819  cvmlift3lem2  29822  cvmlift3lem5  29825  cvmlift3lem6  29826  cvmlift3lem7  29827  cvmlift3lem9  29829  cvmlift3  29830  mrsubfval  29925  msubffval  29940  msubfval  29941  mvhfval  29950  msubff1  29973  mclsval  29980  shftvalg  30143  neibastop3  30794  tailval  30805  filnetlem4  30813  bj-finsumval0  31438  poimirlem1  31635  poimirlem2  31636  poimirlem3  31637  poimirlem4  31638  poimirlem6  31640  poimirlem7  31641  poimirlem10  31644  poimirlem11  31645  poimirlem12  31646  poimirlem13  31647  poimirlem14  31648  poimirlem16  31650  poimirlem19  31653  poimirlem23  31657  poimirlem27  31661  poimirlem29  31663  poimirlem31  31665  poimirlem32  31666  poimir  31667  broucube  31668  ftc2nc  31720  cocanfo  31738  f1ocan2fv  31748  upixp  31750  sdclem2  31765  rrncmslem  31858  ismrer1  31864  lshpset  32243  lsatset  32255  lkrval  32353  eqlkr  32364  ldualvaddval  32396  ldualvsval  32403  ldualvsubval  32422  cmtfvalN  32475  isoml  32503  pmapval  33021  pclvalN  33154  polfvalN  33168  polvalN  33169  psubclsetN  33200  watfvalN  33256  watvalN  33257  ldilset  33373  ltrnfset  33381  ltrnset  33382  dilfsetN  33417  dilsetN  33418  trnfsetN  33420  trnsetN  33421  trlfset  33425  trlset  33426  trlval  33427  ltrnideq  33440  cdlemd8  33470  cdlemg1idlemN  33838  cdlemg1fvawlemN  33839  cdlemg2idN  33862  trlcoabs2N  33988  tgrpfset  34010  tgrpset  34011  tendofset  34024  tendoset  34025  erngfset  34065  erngset  34066  erngfset-rN  34073  erngset-rN  34074  cdlemi2  34085  cdlemj1  34087  cdlemk2  34098  cdlemk4  34100  cdlemk8  34104  cdlemkuu  34161  cdlemk31  34162  cdlemkuv2-3N  34165  cdlemk18-3N  34166  cdlemk22-3  34167  cdlemkfid2N  34189  cdlemkyu  34193  cdlemk19ylem  34196  cdlemk46  34214  cdlemk49  34217  cdlemk43N  34229  cdlemk19u1  34235  cdlemk19u  34236  dvafset  34270  dvaset  34271  dvaplusgv  34276  diaffval  34297  diafval  34298  diaval  34299  dvhfset  34347  dvhset  34348  dvhlveclem  34375  docaffvalN  34388  docafvalN  34389  docavalN  34390  djaffvalN  34400  djafvalN  34401  dibffval  34407  dibfval  34408  dibval  34409  dicffval  34441  dicfval  34442  dicval  34443  dicelvalN  34445  dicvaddcl  34457  dicvscacl  34458  cdlemn8  34471  cdlemn9  34472  dihordlem7b  34482  dihffval  34497  dihfval  34498  dihval  34499  dihopelvalcpre  34515  dihmeetlem1N  34557  dihglblem5apreN  34558  dihmeetlem4preN  34573  dihmeetlem13N  34586  dih1dimatlem0  34595  dochffval  34616  dochfval  34617  dochval  34618  djhffval  34663  djhfval  34664  lcfl7lem  34766  lclkrlem2k  34784  lclkrlem2u  34794  lcdfval  34855  lcdval  34856  lcdvaddval  34865  lcdvsval  34871  lcd0vvalN  34880  lcdvsubval  34885  lcdlsp  34888  mapdffval  34893  mapdfval  34894  mapdval  34895  hvmapffval  35025  hvmapfval  35026  hvmapval  35027  hvmapvalvalN  35028  hvmapidN  35029  hvmaplkr  35035  hdmap1ffval  35063  hdmap1fval  35064  hdmap1vallem  35065  hdmapffval  35096  hdmapfval  35097  hdmapval  35098  hdmapevec2  35106  hgmapffval  35155  hgmapfval  35156  hgmapval  35157  hdmaplna2  35180  hdmapglnm2  35181  hdmapinvlem3  35190  hlhilset  35204  hlhilipval  35219  isnacs  35245  mzpsubst  35289  eldioph2  35303  pw2f1ocnv  35588  fnwe2lem2  35605  islnr3  35670  hbtlem1  35678  hbtlem2  35679  hbtlem7  35680  hbtlem4  35681  hbtlem5  35683  hbt  35685  dgrsub2  35690  mpaaeu  35705  mpaalem  35707  rgspnval  35723  flcidc  35729  cntzsdrg  35757  itgpowd  35788  binomcxplemdvsum  36331  binomcxplemnotnn0  36332  addrfv  36449  subrfv  36450  mulvfv  36451  refsum2cnlem1  36988  n0p  37006  fvmpt2bd  37046  fmuldfeqlem1  37222  fmuldfeq  37223  fmul01lt1lem1  37224  fmul01lt1lem2  37225  limciccioolb  37263  limcicciooub  37279  cncfuni  37326  cncfiooicclem1  37333  dvsinax  37345  dvbdfbdioolem1  37362  dvnmptdivc  37372  dvnmul  37377  dvnprodlem1  37380  dvnprodlem2  37381  dvnprodlem3  37382  dvnprod  37383  itgsincmulx  37410  stoweidlem17  37436  stoweidlem20  37439  stoweidlem27  37446  stoweidlem31  37451  stoweidlem34  37454  stoweidlem44  37464  stoweidlem48  37468  stoweidlem59  37479  stirlinglem3  37497  stirlinglem15  37509  dirkeritg  37523  dirkercncflem2  37525  dirkercncflem3  37526  dirkercncflem4  37527  dirkercncf  37528  fourierdlem42  37570  fourierdlem60  37588  fourierdlem61  37589  fourierdlem68  37596  fourierdlem73  37601  fourierdlem80  37608  fourierdlem93  37621  fourierdlem94  37622  fourierdlem103  37631  fourierdlem104  37632  fourierdlem111  37639  fourierdlem112  37640  fourierdlem113  37641  elaa2lem  37655  elaa2  37656  etransclem17  37673  etransclem29  37685  etransclem32  37688  etransclem46  37702  sge0f1o  37748  nnfoctbdjlem  37792  pfxfv  38320  rngcid  38729  ringcid  38775  funcringcsetcALTV2lem6  38791  funcringcsetclem6ALTV  38814  coe1sclmulval  38927  ply1mulgsum  38932  evl1at0  38933  evl1at1  38934  lincvalpr  38961  aacllem  39291
  Copyright terms: Public domain W3C validator