Theorem eqidd 2740

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	⊢ (𝜑 → 𝐴 = 𝐴)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2739	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  nfabd2  2924  neleq1  3044  neleq2  3045  elabd3  3609  nelrdva  3646  sbcbidv  3778  csbie2df  4372  reusngf  4607  rexreusng  4612  reuprg0  4635  iunxdif3  5025  mpteq1  5162  mpteq1i  5164  mpteq2da  5165  mpteq2dva  5166  nfcvb  5306  dfid2  5516  feq23d  6651  f10d  6802  fvmptdv2  6955  elrnrexdm  7031  f1ossf1o  7071  fmptco  7072  cofmpt  7075  fprg  7099  ftpg  7100  fmptsng  7113  fmptsnd  7114  f1dom3fv3dif  7213  f1dom3el3dif  7214  fliftfun  7257  fliftval  7261  nfriotad  7325  cbvmpo  7451  fconstmpo  7474  eqfnov2  7487  ovmpod  7509  ovmpodv2  7515  fvmpopr2d  7519  elovmporab  7603  elovmporab1w  7604  elovmporab1  7605  ovmpt3rab1  7615  elovmpt3rab  7618  ofval  7632  ofrval  7633  offn  7634  fnfvof  7638  off  7639  ofres  7640  coof  7645  ofco  7646  caofref  7652  caofid0l  7654  caofid0r  7655  caofid1  7656  caofid2  7657  caofrss  7660  caoftrn  7662  tfisi  7800  fsplitfpar  8058  fczsupp0  8134  suppssof1  8140  suppofss1d  8145  suppofss2d  8146  fvmpocurryd  8212  fpr3g  8226  iserd  8661  fsetfocdm  8799  ixpsnf1o  8877  mapxpen  9072  dffi3  9335  cantnf0  9588  cantnfp1  9594  cantnflem1  9602  ttrcltr  9629  axcclem  10371  ttukeylem3  10425  fpwwe2lem8  10553  ofsubeq0  12148  ofnegsub  12149  ofsubge0  12150  fzo0to3tp  13699  fzo1to4tp  13701  modsubmod  13883  seqid  14001  seqid2  14002  seqz  14004  seqof  14013  elovmptnn0wrd  14513  ccatdmss  14536  ccatws1ls  14588  pfxsuffeqwrdeq  14652  wrdind  14676  wrd2ind  14677  ccats1pfxeqbi  14696  repswsymb  14728  repswsymball  14733  repswsymballbi  14734  s3eq2  14824  swrds2m  14895  wrdl2exs2  14900  swrd2lsw  14906  wwlktovfo  14912  s3sndisj  14921  s3iunsndisj  14922  relexp0g  14976  relexpsucnnr  14979  relexp1g  14980  rtrclreclem1  15011  rtrclreclem4  15015  dfrtrcl2  15016  rlim2  15450  climcl  15453  rlimcl  15457  clim2  15458  rlimclim1  15499  rlimclim  15500  climrlim2  15501  climuni  15506  rlimres  15512  climeq  15521  2clim  15526  climshftlem  15528  climabs0  15539  climcn1  15546  climcn2  15547  o1of2  15567  o1rlimmul  15573  o1add2  15578  o1mul2  15579  o1sub2  15580  o1dif  15584  climsqz  15595  climsqz2  15596  rlimdiv  15600  isercoll  15622  climsup  15624  climcau  15625  caurcvgr  15628  caucvgb  15634  serf0  15635  iseralt  15639  sumz  15676  fsumss  15679  fsumsplitsn  15698  fsumsplit1  15699  fsumsplitsnun  15709  isumclim3  15713  isummulc2  15716  fsum2dlem  15724  fsumconst  15744  fsumabs  15756  fsumparts  15761  fsumrlim  15766  fsumo1  15767  seqabs  15769  cvgcmpce  15773  fsumiun  15776  ackbijnn  15785  isumshft  15796  isumltss  15805  climcndslem1  15806  climcndslem2  15807  climcnds  15808  mertenslem1  15841  mertenslem2  15842  prod1  15901  fprodss  15905  fprodconst  15935  fprod2dlem  15937  fprodsplitsn  15946  iprodclim3  15957  eftlcl  16066  reeftlcl  16067  eftlub  16068  efsep  16069  effsumlt  16070  eirrlem  16163  rpnnen2lem6  16178  rpnnen2lem7  16179  rpnnen2lem8  16180  rpnnen2lem9  16181  rpnnen2lem12  16184  2tp1odd  16313  sadasslem  16431  smupvallem  16444  smumul  16454  alginv  16536  algfx  16541  cncongr1  16628  qnumdencoprm  16707  qeqnumdivden  16708  vdwlem1  16944  vdwlem12  16955  vdwlem13  16956  prmodvdslcmf  17010  prmgap  17022  prmgaplcm  17023  prmgapprmo  17025  setsexstruct2  17137  setsstruct  17138  prdssca  17411  prdsbas  17412  prdsplusg  17413  prdsmulr  17414  prdsvsca  17415  prdsip  17416  prdsle  17417  prdsds  17419  prdstset  17421  prdshom  17422  prdsco  17423  prdsvscafval  17435  prdsdsval2  17439  prdsdsval3  17440  pwsle  17448  pwsleval  17449  pwsvscaval  17451  imasbas  17468  imasds  17469  imasplusg  17473  imasmulr  17474  imassca  17475  imasvsca  17476  imasip  17477  imastset  17478  imasle  17479  imasvscafn  17493  imasvscaval  17494  qusin  17500  xpsvsca  17533  iscat  17630  iscatd  17631  iscatd2  17639  0catg  17646  homfeq  17652  homfeqd  17653  comfffval2  17659  comffval2  17660  comfeq  17664  comfeqd  17665  oppccatid  17677  2oppccomf  17683  moni  17695  rcaninv  17753  ssc2  17781  ssctr  17784  ssceq  17785  subcssc  17799  subccat  17807  subsubc  17812  funcres  17855  funcres2  17857  idfusubc  17859  funcres2c  17862  idffth  17894  cofull  17895  cofth  17896  ressffth  17899  isnat  17909  fuccofval  17921  fuccatid  17931  fucpropd  17939  elhomai  17992  coafval  18023  setcval  18036  setcbas  18037  setchomfval  18038  setccofval  18041  setcco  18042  setccatid  18043  setcepi  18047  funcsetcres2  18052  catcval  18059  catcbas  18060  catchomfval  18061  catccofval  18063  catcco  18064  catccatid  18065  catcfuccl  18077  estrcval  18082  estrcbas  18083  estrchomfval  18084  estrccofval  18087  estrcco  18088  estrccatid  18090  estrreslem2  18096  fullestrcsetc  18109  fullsetcestrc  18124  xpcbas  18136  xpchomfval  18137  xpccofval  18140  xpccatid  18146  prfval  18157  catcxpccl  18165  xpcpropd  18166  evlfval  18175  curfval  18181  curf1  18183  curf12  18185  curf2  18187  curf2val  18188  hofval  18210  hof2fval  18213  hofcllem  18216  oppchofcl  18218  oppcyon  18227  oyoncl  18228  yonedalem4a  18233  yonedalem4b  18234  yonedainv  18239  oduposb  18285  joinval  18333  meetval  18347  isdlat  18480  ipopos  18494  pfxchn  18568  chnind  18579  chnso  18582  chnccats1  18583  chnccat  18584  chnrev  18585  gsumpropd  18638  gsumpropd2lem  18639  gsumval1  18643  gsumval2a  18645  issgrp  18680  issgrpd  18690  prdssgrpd  18693  ismndd  18716  mndprop  18720  prdsmndd  18730  imasmnd2  18734  insubm  18778  mhmima  18785  frmdbas  18812  frmdmnd  18819  efmnd  18830  smndex1gid  18864  smndex1gidOLD  18865  smndex1n0mnd  18875  smndex2dlinvh  18880  sgrpnmndex  18895  resgrpplusfrn  18918  grpprop  18920  grpsubfval  18951  grpsubfvalALT  18952  grpsubpropd  19013  prdsgrpd  19018  imasgrp2  19023  imasgrp  19024  imasgrpf1  19025  mulgfval  19037  mulgfvalALT  19038  mulgnngsum  19047  mulgnn0gsum  19048  mulgpropd  19084  subgsub  19106  eqgfval  19143  qusgrp  19153  ghmqusnsglem1  19247  ghmqusnsglem2  19248  ghmqusnsg  19249  ghmquskerlem1  19250  ghmquskerlem2  19252  ghmquskerlem3  19253  ghmqusker  19254  oppgmnd  19321  oppgmndb  19322  oppggrp  19324  oppggrpb  19325  symgval  19338  symg1bas  19358  symg2bas  19360  symgvalstruct  19364  symggrp  19367  gsmsymgrfixlem1  19394  gsmsymgreqlem2  19398  symgfixels  19401  symgsssg  19434  symgfisg  19435  psgnunilem4  19464  psgnvalii  19476  oppglsm  19609  lsmelvalmi  19619  efgi0  19687  efgi1  19688  efgtf  19689  efgval2  19691  efginvrel2  19694  frgp0  19727  frgpup3lem  19744  ablprop  19760  subcmn  19804  gex2abl  19818  prdscmnd  19828  qusabl  19832  abl1  19833  cygabl  19858  gsumzf1o  19879  gsumzaddlem  19888  gsumzsplit  19894  gsumconst  19901  gsumconstf  19902  gsummptshft  19903  gsummhm2  19906  gsummptmhm  19907  gsumzunsnd  19923  gsumunsnfd  19924  gsumpt  19929  gsummptf1o  19930  gsummptun  19931  gsum2dlem2  19938  gsumcom2  19942  nn0gsumfz  19951  dprdval  19972  dprdssv  19985  dprdfeq0  19991  dprdsubg  19993  dprdspan  19996  dprdz  19999  subgdmdprd  20003  subgdprd  20004  gsumle  20112  isrng  20127  isrngd  20146  prdsrngd  20149  imasrng  20150  issrg  20161  isring  20210  ringabl  20254  ringprop  20263  isringd  20264  prdsringd  20292  prdscrngd  20293  prds1  20294  pwspjmhmmgpd  20299  imasring  20302  opprrng  20317  opprrngb  20318  opprringb  20320  dvrfval  20374  rnghmf1o  20424  c0mgm  20431  c0mhm  20432  c0snmgmhm  20434  c0snmhm  20435  rngisomring1  20440  rhmf1o  20463  pwsco1rhm  20474  pwsco2rhm  20475  zrrnghm  20509  rhmimasubrng  20539  pwsdiagrhm  20580  rngcbas  20594  rngchomfval  20595  dfrngc2  20601  rnghmsscmap2  20602  rnghmsscmap  20603  rngccat  20607  rngcid  20608  funcrngcsetc  20613  funcrngcsetcALT  20614  zrinitorngc  20615  zrtermorngc  20616  ringcbas  20623  ringchomfval  20624  dfringc2  20630  rhmsscmap2  20631  rhmsscmap  20632  ringccat  20636  ringcid  20637  rngcresringcat  20642  funcringcsetc  20647  zrtermoringc  20648  rhmsubc  20662  drngprop  20717  isdrngd  20738  isdrngrd  20739  isdrngdOLD  20740  isdrngrdOLD  20741  abvtrivd  20805  idsrngd  20829  suborng  20849  islmodd  20857  lmodabl  20900  lss1  20929  lsssn0  20939  islss3  20950  lss1d  20954  lssintcl  20955  prdslmodd  20960  idlmhm  21032  invlmhm  21033  lmhmvsca  21036  lbsextlem2  21153  sralmod  21178  sralmod0  21179  rlm0  21186  rlmvneg  21197  rnglidlmsgrp  21240  rnglidlrng  21241  qus2idrng  21267  crngridl  21274  quscrng  21277  rhmqusnsg  21279  rngqiprngimf1lem  21288  rngqiprngimf1  21294  absabv  21400  pzriprnglem10  21466  zrhpropd  21490  fermltlchr  21505  znzrh  21518  znbas  21519  zncrng  21520  znzrhfo  21523  znf1o  21527  frgpcyg  21549  evpmodpmf1o  21572  isphld  21630  phlpropd  21631  phssip  21634  phlssphl  21635  pjfval  21682  dsmmval  21710  dsmmsubg  21719  frlmip  21754  frlmipval  21755  frlmphllem  21756  frlmphl  21757  islindf  21788  islindf4  21814  isassa  21832  isassad  21841  issubassa3  21842  asclfval  21854  ressascl  21872  psrval  21891  psrbaglesupp  21898  psrbagcon  21901  psrbaglefi  21902  psrbagleadd1  21904  psrbagconf1o  21905  gsumbagdiaglem  21907  psrass1lem  21909  psrbas  21910  psrplusg  21913  psrmulr  21918  psrsca  21923  psrvscafval  21924  psrvscaval  21926  psrlmod  21935  psrlidm  21937  psrdi  21940  psrdir  21941  psrcom  21943  psrring  21945  psrassa  21948  mplsubglem  21974  mpllsslem  21975  mplvscaval  21991  mplcoe1  22014  mplcoe3  22015  mplcoe5  22017  opsrcrng  22036  opsrassa  22037  mplmon2  22038  evlslem2  22056  evlslem1  22059  evlsvvval  22070  mplmapghm  22099  evlsmaprhm  22108  selvvvval  22119  selvadd  22120  selvmul  22121  mhpmulcl  22138  psdffval  22146  psdmplcl  22151  psdadd  22152  psdmul  22155  psdmvr  22158  ply1lss  22182  ply1subrg  22183  opsr0  22204  opsr1  22205  subrgply1  22218  psrplusgpropd  22221  psropprmul  22223  opsrring  22230  opsrlmod  22231  ply1mpl0  22242  ply1mpl1  22244  coe1z  22250  coe1mul2  22256  coe1tm  22260  coe1sclmulfv  22270  ply1coe  22285  evls1rhm  22309  evls1sca  22310  evl1rhm  22319  evl1sca  22321  evl1expd  22332  evl1gsumdlem  22343  evl1varpw  22348  evls1maplmhm  22364  mamufval  22376  mamudi  22387  mamudir  22388  mat0  22401  matinvg  22402  matlmod  22413  matinvgcell  22419  matring  22427  matassa  22428  mat0dimcrng  22454  mat1dim0  22457  mat1f1o  22462  dmatmulcl  22484  scmatval  22488  scmatscmiddistr  22492  scmataddcl  22500  scmatsubcl  22501  scmatmulcl  22502  scmatlss  22509  scmatrhmcl  22512  1mavmul  22532  mavmul0  22536  marepvfval  22549  submafval  22563  submaval  22565  mdetleib2  22572  mdet0pr  22576  m1detdiag  22581  mdetrsca  22587  mdetrsca2  22588  mdetrlin2  22591  mdetralt  22592  mdetralt2  22593  mdetunilem2  22597  mdetunilem5  22600  mdetunilem9  22604  mdetuni0  22605  m2detleib  22615  madufval  22621  symgmatr01lem  22637  symgmatr01  22638  gsummatr01lem3  22641  gsummatr01lem4  22642  gsummatr01  22643  smadiadetlem3  22652  smadiadetglem2  22656  smadiadetr  22659  mat2pmatghm  22714  cpm2mfval  22733  m2cpminvid  22737  m2cpminvid2lem  22738  m2cpminvid2  22739  decpmatval  22749  decpmataa0  22752  decpmatmul  22756  pmatcollpw1  22760  pmatcollpw2lem  22761  monmatcollpw  22763  pmatcollpwlem  22764  pmatcollpw  22765  pmatcollpwscmatlem2  22774  pm2mpval  22779  pm2mpcl  22781  pm2mpf1  22783  mptcoe1matfsupp  22786  mp2pm2mplem3  22792  mp2pm2mplem4  22793  pm2mpghm  22800  pm2mpmhmlem2  22803  chpmat1dlem  22819  chp0mat  22830  fvmptnn04ifa  22834  fvmptnn04ifb  22835  fvmptnn04ifc  22836  fvmptnn04ifd  22837  cpmadugsumlemB  22858  chcoeffeqlem  22869  epttop  22993  ordtbas2  23175  ordtopn1  23178  ordtopn2  23179  lmss  23282  2ndci  23432  2ndcsep  23443  dis2ndc  23444  1stcelcls  23445  dissnlocfin  23513  ptbasid  23559  xkoopn  23573  prdstopn  23612  ptrescn  23623  txlm  23632  lmcn2  23633  tx1stc  23634  xkopt  23639  cnmpt2c  23654  cnmptk1  23665  cnmpt1k  23666  cnmptkk  23667  qtopeu  23700  txswaphmeolem  23788  xpstopnlem1  23793  ptcmpfi  23797  xkohmeo  23799  rnelfmlem  23936  rnelfm  23937  hauspwpwf1  23971  lmflf  23989  flfcnp2  23991  alexsubb  24030  tmdgsum  24079  tgpconncomp  24097  qustgphaus  24107  tsmsfbas  24112  tsmspropd  24116  tsmssplit  24136  tsmsxplem1  24137  tsmsxplem2  24138  ustuqtop4  24228  imasdsf1olem  24357  blfvalps  24367  stdbdxmet  24499  met2ndci  24506  prdsxmslem2  24513  metustexhalf  24540  cfilucfil  24543  restmetu  24554  nmfval  24572  nmpropd  24578  nmpropd2  24579  subgnm  24617  tng0  24627  tngnm  24635  tnggrpr  24639  tngngp3  24640  tngnrg  24658  sranlm  24668  qdensere  24753  mpomulcn  24853  fsumcn  24856  cncfcompt2  24894  cncfmpt1f  24900  negfcncf  24909  oprpiece1res2  24938  htpyid  24963  phtpyid  24975  pcofval  24996  pcopt2  25009  om1bas  25017  om1plusg  25020  om1tset  25021  pi1bas  25024  pi1bas2  25027  pi1eluni  25028  pi1bas3  25029  pi1cpbl  25030  pi1addf  25033  pi1addval  25034  pi1grplem  25035  pi1xfr  25041  pi1xfrcnvlem  25042  pi1coghm  25047  cphassr  25198  tcphphl  25213  ipcau2  25220  cphipval  25229  lmnn  25249  iscau  25262  cmetcaulem  25274  iscmet3lem1  25277  causs  25284  lmclim  25289  srabn  25346  rrxprds  25375  rrxip  25376  rrxcph  25378  rrxds  25379  rrxmvallem  25390  rrxmval  25391  rrxdsfival  25399  ehl2eudisval  25409  divcncf  25433  ovollb2lem  25474  ovolfiniun  25487  ovolicc2lem4  25506  shftmbl  25524  volfiniun  25533  ioombl1lem4  25547  uniioombllem2  25569  uniioombllem6  25574  vitalilem4  25597  mbfmulc2lem  25633  mbfmulc2re  25634  mbfneg  25636  mbfaddlem  25646  mbfadd  25647  mbfsub  25648  mbfmulc2  25649  0plef  25658  0pledm  25659  itg1ge0  25672  i1faddlem  25679  i1fmullem  25680  i1fmulclem  25688  itg1mulc  25690  itg1lea  25698  itg1le  25699  mbfi1flimlem  25708  mbfmullem2  25710  mbfmul  25712  xrge0f  25717  itg2ge0  25721  itg2const  25726  itg2const2  25727  itg2uba  25729  itg2lea  25730  itg2splitlem  25734  itg2split  25735  itg2monolem1  25736  itg2mono  25739  itg2i1fseqle  25740  itg2i1fseq  25741  itg2addlem  25744  itg2gt0  25746  itg2cnlem1  25747  itg2cnlem2  25748  isibl2  25752  iblitg  25754  itgcl  25770  ibl0  25773  iblcnlem1  25774  itgcnlem  25776  iblss  25791  iblss2  25792  i1fibl  25794  itgitg1  25795  itgle  25796  itgeqa  25800  iblconst  25804  ibladdlem  25806  ibladd  25807  itgaddlem1  25809  itgfsum  25813  iblabslem  25814  iblabs  25815  iblabsr  25816  iblmulc2  25817  itgmulc2lem1  25818  itgsplit  25822  bddmulibl  25825  bddibl  25826  bddiblnc  25828  limccnp2  25878  limcco  25879  dvidlem  25901  dvcnp2  25906  dvaddbr  25924  dvmulbr  25925  dvaddf  25928  dvcmulf  25931  dvexp  25939  dvmptadd  25946  dvmptmul  25947  dvmptco  25958  dvmptfsum  25961  dvcnvlem  25962  dvef  25966  rolle  25976  mvth  25978  dvlip  25979  dvlipcn  25980  lhop1lem  25999  itgsubstlem  26034  itgpowd  26036  ply1divalg2  26123  uc1pmon1p  26136  q1pval  26139  r1pval  26142  elply2  26180  elplyr  26185  plypf1  26196  plyaddlem1  26197  coeeulem  26208  plyco  26225  coeaddlem  26233  coemulc  26239  dgradd2  26252  dgrcolem1  26257  dgrcolem2  26258  dgrco  26259  ofmulrt  26267  plydivlem3  26280  plydivlem4  26281  plyrem  26290  iaa  26310  aareccl  26311  aannenlem2  26314  aaliou3lem3  26329  aaliou3lem7  26334  taylfval  26343  taylply2  26352  dvntaylp  26355  taylthlem2  26358  ulmclm  26371  ulmres  26372  ulmshftlem  26373  ulm0  26375  ulmcau  26379  ulmss  26381  ulmbdd  26382  ulmcn  26383  mtest  26388  mtestbdd  26389  iblulm  26391  itgulm  26392  pserulm  26406  pserdvlem2  26412  abelthlem5  26419  abelthlem6  26420  abelthlem8  26423  abelthlem9  26424  sincn  26428  coscn  26429  efcvx  26433  efabl  26533  logfac  26584  logcn  26630  chordthmlem  26815  chordthmlem5  26819  mcubic  26830  leibpi  26925  efrlim  26952  amgmlem  26972  lgamgulmlem2  27012  basellem7  27069  basellem9  27071  musum  27173  chtublem  27193  logexprlim  27207  dchrbas  27217  dchr1cl  27233  dchrabl  27236  dchrfi  27237  dchrhash  27253  bposlem6  27271  lgsdir2lem5  27311  gausslemma2dlem1  27348  lgseisenlem2  27358  lgseisenlem3  27359  lgseisenlem4  27360  lgsquad2lem2  27367  2lgslem1b  27374  2lgslem3b1  27383  2lgslem3c1  27384  2lgsoddprmlem4  27397  2sqlem8  27408  2sqlem11  27411  2sqreulem1  27428  2sqreunnlem1  27431  chtppilimlem2  27456  chebbnd2  27459  chpchtlim  27461  chpo1ub  27462  vmadivsum  27464  rpvmasumlem  27469  dchrisum0re  27495  dchrisum0  27502  mudivsum  27512  selberglem1  27527  selberglem2  27528  selberg2lem  27532  selberg2  27533  pntrsumo1  27547  selbergr  27550  abvcxp  27597  nosupfv  27689  noinffv  27704  madecut  27894  elons2  28269  oncutlt  28275  oniso  28282  seqsfn  28320  seqs1  28321  seqsp1  28322  n0fincut  28366  zcuts  28418  twocut  28434  expsval  28436  pw2cut2  28473  z12addscl  28488  z12shalf  28491  z12zsodd  28493  istrkgld  28546  istrkg2ld  28547  tgsegconeq  28573  tgbtwnouttr2  28582  ercgrg  28604  cgr3id  28606  tgbtwnxfr  28617  motgrp  28630  tgbtwnconn1lem3  28661  legov  28672  legid  28674  btwnleg  28675  legbtwn  28681  mirreu3  28741  mirinv  28753  miduniq1  28773  colmid  28775  krippenlem  28777  israg  28784  ragcgr  28794  motrag  28795  perpneq  28801  isperp2  28802  isperp2d  28803  footexALT  28805  footexlem1  28806  footexlem2  28807  foot  28809  perprag  28813  perpdragALT  28814  colperpexlem1  28817  mideulem2  28821  opphllem2  28835  opphllem3  28836  opphllem4  28837  midbtwn  28866  midcom  28869  mirmid  28870  lmieu  28871  lmif  28872  islmib  28874  lmilmi  28876  lmieq  28878  lmiinv  28879  lmiisolem  28883  hypcgrlem1  28886  hypcgrlem2  28887  lmiopp  28889  trgcopyeu  28893  iscgra  28896  iscgra1  28897  iscgrad  28898  sacgr  28918  isinag  28925  isinagd  28926  inagflat  28927  inaghl  28932  isleag  28934  isleagd  28935  ttgval  28962  cchhllem  28974  usgredg4  29305  ushgredgedg  29317  ushgredgedgloop  29319  usgrstrrepe  29323  uspgr1e  29332  uhgrspan1  29391  usgrres1  29403  nbgrnself  29447  nbusgredgeu  29454  cusgrfilem2  29544  finsumvtxdg2size  29638  finsumvtxdgeven  29640  wlk1walk  29726  uspgr2wlkeq  29733  uspgr2wlkeqi  29735  wlkonwlk  29748  wlkonwlk1l  29749  usgr2trlncl  29847  crctcshwlkn0lem7  29903  wwlksnredwwlkn  29982  wwlksnextbij  29989  wwlksnextprop  29999  wwlksnwwlksnon  30002  elwwlks2ons3im  30041  clwlkclwwlk2  30092  clwlkclwwlkfo  30098  clwlkclwwlkf1  30099  clwwlkwwlksb  30143  clwlknf1oclwwlkn  30173  clwwlknonmpo  30178  clwwlknonex2lem2  30197  0pthon1  30217  uhgr3cyclex  30271  iseupth  30290  eupth0  30303  eupth2lem2  30308  frgr3vlem1  30362  3vfriswmgrlem  30366  2clwwlk2clwwlklem  30435  wlkl0  30456  numclwlk1lem2  30459  grpodivfval  30624  dipfval  30792  ipval2  30797  lnoval  30842  minvecolem3  30966  h2hcau  31069  h2hlm  31070  opsqrlem3  32232  opsqrlem4  32233  foresf1o  32593  disjnf  32660  disjdifprg  32665  iundisjf  32679  br8d  32701  fnfvor  32702  ofrco  32703  ofrn2  32733  off2  32734  ofresid  32735  fmptcof2  32750  aciunf1  32756  ofpreima  32758  f1ocnt  32893  sgnneg  32926  prodindf  32942  indf1ofs  32946  wrdfsupp  33017  wrdpmcl  33018  pfxf1  33022  s1f1  33023  wrdt2ind  33033  swrdrn2  33034  ressnm  33044  abvpropd2  33045  ismntd  33064  dfmgc2lem  33075  pwrssmgc  33080  gsummpt2d  33131  gsummptf1od  33137  gsummptfsf1o  33142  gsumhashmul  33149  gsumwrd2dccat  33160  wrdpmtrlast  33175  psgnfzto1stlem  33182  fzto1st1  33184  tocycfv  33191  cycpmcl  33198  tocycf  33199  tocyc01  33200  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem1  33208  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  cycpm3cl2  33218  cycpmconjv  33224  tocyccntz  33226  cyc3evpm  33232  cyc3genpm  33234  cycpmgcl  33235  cycpmconjslem2  33237  cyc3conja  33239  sgnsv  33242  inftmrel  33262  isinftm  33263  submarchi  33268  isslmd  33284  urpropd  33313  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspn  33328  elrgspnsubrun  33331  erlval  33340  rlocval  33341  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  rloccring  33352  resv0g  33422  resvcmn  33424  imaslmod  33437  imasmhm  33438  imasghm  33439  imasrhm  33440  imaslmhm  33441  znfermltl  33450  islinds5  33451  ellspds  33452  linds2eq  33465  lindfpropd  33466  elringlsmd  33478  nsgmgclem  33495  nsgmgc  33496  rhmquskerlem  33509  elrspunsn  33513  idlinsubrg  33515  qsidomlem1  33536  qsidomlem2  33537  opprqusbas  33572  qsdrngi  33579  dflring2  33585  rprmval  33608  rprmnz  33612  rprmnunit  33613  unitmulrprm  33620  1arithidomlem1  33627  1arithidomlem2  33628  1arithidom  33629  1arithufdlem3  33638  dfufd2lem  33641  ply1dg1rt  33672  ply1mulrtss  33674  ply1degltlss  33688  ply1gsumz  33691  r1pquslmic  33703  0mplrim  33707  selvply1rhmlemb  33712  selvply1rhmlem2  33714  selvply1rhmlem4  33716  mplvrpmfgalem  33737  psrmonprod  33745  esplyfvaln  33767  esplyind  33768  vietalem  33772  sra1r  33774  sradrng  33775  sraidom  33776  srasubrg  33777  resssra  33780  drgext0g  33783  drgextlsp  33787  rlmdim  33803  tnglvec  33805  tngdim  33806  matdim  33808  ply1degltdimlem  33815  lbsdiflsp0  33819  dimkerim  33820  fedgmullem2  33823  lactlmhm  33827  extdg1id  33859  ccfldsrarelvec  33864  ccfldextdgrr  33865  fldextrspunlsplem  33866  fldextrspunlsp  33867  fldextrspunlem1  33868  fldextrspunfld  33869  fldextrspunlem2  33870  extdgfialglem1  33885  extdgfialglem2  33886  irredminply  33909  algextdeglem3  33912  algextdeglem4  33913  algextdeglem8  33917  constrsslem  33934  constrext2chnlem  33943  constrcon  33967  2sqr3nconstr  33974  cos9thpinconstrlem2  33983  1smat1  33997  submatres  33999  submateq  34002  lmatcl  34009  mdetlap1  34019  madjusmdetlem3  34022  circtopn  34030  locfinref  34034  tpr2rico  34105  lmdvglim  34147  qqhval  34165  esumeq1  34227  esumeq1d  34228  esumeq2d  34230  esumf1o  34243  esumsplit  34246  esumadd  34250  gsumesum  34252  esumlub  34253  esumaddf  34254  esumcst  34256  esumsnf  34257  esumpinfval  34266  esumcocn  34273  esummulc1  34274  esumcvg  34279  esum2d  34286  ofcval  34292  ofcfn  34293  ofcfeqd2  34294  ofcf  34296  ofcfval4  34298  ofcof  34300  sigapildsys  34355  sxval  34383  measvunilem0  34406  measvuni  34407  measiun  34411  meascnbl  34412  measinb  34414  volmeas  34424  sxbrsiga  34483  omssubadd  34493  fiunelcarsg  34509  itgeq12dv  34519  sitgval  34525  eulerpartlems  34553  eulerpartgbij  34565  eulerpartlemn  34574  sseqf  34585  sseqp1  34588  totprobd  34619  probfinmeasb  34621  probmeasb  34623  rrvadd  34645  dstfrvclim1  34671  gsumnunsn  34734  plymul02  34739  plymulx  34741  signsply0  34744  fdvneggt  34793  fdvnegge  34795  itgexpif  34799  reprpmtf1o  34819  circlemethhgt  34836  logdivsqrle  34843  hgt750lemg  34847  hgt750lemb  34849  hgt750lema  34850  f1resfz0f1d  35351  2cycl2d  35376  quartfull  35402  sconnpi1  35476  cvmliftphtlem  35554  cvmlift3lem2  35557  satfv1  35600  satfdmlem  35605  satf0suc  35613  satf0op  35614  sat1el2xp  35616  fmla  35618  fmlasuc0  35621  fmlafvel  35622  fmlasuc  35623  fmla1  35624  satffunlem1lem2  35640  satffunlem2lem2  35643  sategoelfvb  35656  satfv1fvfmla1  35660  2goelgoanfmla1  35661  elmsubrn  35765  msubco  35768  mthmpps  35819  r1peuqusdeg1  35880  sinccvg  35910  circum  35911  br8  35993  br4  35995  brsegle  36345  hilbert1.1  36391  itgeq2sdv  36457  ditgeq3sdv  36460  cbvoprab23davw  36513  cbvoprab13davw  36514  trer  36553  knoppcnlem4  36811  knoppcnlem9  36816  knoppcnlem11  36818  knoppndvlem6  36832  knoppf  36850  bj-imdirco  37559  bj-fvmptunsn2  37627  bj-finsumval0  37654  exrecfnlem  37750  finxpreclem1  37760  matunitlindflem1  37992  matunitlindflem2  37993  poimirlem1  37997  poimirlem2  37998  poimirlem3  37999  poimirlem4  38000  poimirlem5  38001  poimirlem6  38002  poimirlem7  38003  poimirlem10  38006  poimirlem11  38007  poimirlem12  38008  poimirlem16  38012  poimirlem17  38013  poimirlem19  38015  poimirlem20  38016  poimirlem22  38018  poimirlem23  38019  poimirlem28  38024  poimirlem29  38025  poimirlem31  38027  broucube  38030  mblfinlem2  38034  volsupnfl  38041  itg2addnclem  38047  itg2addnclem3  38049  itg2addnc  38050  itg2gt0cn  38051  ibladdnclem  38052  itgaddnclem1  38054  itgaddnc  38056  iblabsnclem  38059  iblabsnc  38060  iblmulc2nc  38061  itgmulc2nclem1  38062  itgmulc2nclem2  38063  itgmulc2nc  38064  ftc1anclem2  38070  ftc1anclem4  38072  ftc1anclem5  38073  ftc1anclem6  38074  ftc1anclem7  38075  ftc1anclem8  38076  ftc1anc  38077  areacirc  38089  unirep  38090  upixp  38105  sdc  38120  lmclim2  38134  geomcau  38135  caures  38136  caushft  38137  prdsbnd2  38171  heibor1lem  38185  bfplem2  38199  rrncmslem  38208  isrngo  38273  iuneq2f  38532  dmec2d  38687  lflset  39560  islfld  39563  lfladdcl  39572  lflvscl  39578  lkrsc  39598  eqlkr2  39601  lshpkrlem1  39611  ldualset  39626  ldualvaddval  39632  ldualvsval  39639  ldualgrplem  39646  lduallmodlem  39653  cmtfvalN  39711  isoml  39739  iscvlat  39824  llni2  40013  lplni2  40038  lvoli3  40078  lvoli2  40082  paddfval  40298  lhpset  40496  ltrnfset  40618  trlfset  40661  cdleme21k  40839  cdlemeiota  41086  tgrpfset  41245  tgrpset  41246  tgrpabl  41252  tendo0cbv  41287  tendo02  41288  erngfset  41300  erngset  41301  erngfset-rN  41308  erngset-rN  41309  cdlemkid5  41436  cdlemkid  41437  dvafset  41505  dvaset  41506  diaffval  41531  dialss  41547  diaf11N  41550  dvhfset  41581  dvhset  41582  docaffvalN  41622  dibfval  41642  dibf11N  41662  diblss  41671  diclss  41694  dihord2cN  41722  dihord11b  41723  dihffval  41731  dihord6apre  41757  dihglblem2aN  41794  dihglblem2N  41795  dihjatcclem4  41922  lclkrs  42040  mapdh6dN  42240  mapdh6eN  42241  mapdh6fN  42242  mapdh6jN  42246  hvmapffval  42259  hvmapfval  42260  mapdh8a  42276  mapdh8ad  42280  mapdh8d0N  42283  mapdh8d  42284  mapdh8i  42287  mapdh8j  42288  mapdh9a  42290  mapdh9aOLDN  42291  hdmap1l6d  42314  hdmap1l6e  42315  hdmap1l6f  42316  hdmap1l6j  42320  hdmapval2  42333  hdmapeveclem  42335  hdmapval3lemN  42338  hdmap11lem1  42342  hgmapfval  42387  hlhils0  42446  hlhils1N  42447  hlhillvec  42452  hlhildrng  42453  hlhil0  42456  hlhillsm  42457  rhmzrhval  42466  zndvdchrrhm  42467  3factsumint1  42515  lcmineqlem12  42534  aks4d1p1p4  42565  aks4d1p1p7  42568  aks4d1p9  42582  isprimroot  42587  primrootsunit1  42591  posbezout  42594  primrootscoprbij  42596  remexz  42598  aks6d1c1p2  42603  aks6d1c1p3  42604  aks6d1c1p4  42605  aks6d1c1p5  42606  aks6d1c1p7  42607  evl1gprodd  42611  aks6d1c2p2  42613  hashscontpow  42616  aks6d1c2lem4  42621  aks6d1c2  42624  aks6d1c5lem2  42632  aks6d1c5  42633  deg1gprod  42634  2np3bcnp1  42638  2ap1caineq  42639  sticksstones8  42647  sticksstones10  42649  sticksstones12a  42651  sticksstones12  42652  sticksstones17  42657  sticksstones18  42658  sticksstones19  42659  sticksstones21  42661  sticksstones22  42662  aks6d1c6lem1  42664  aks6d1c6lem2  42665  aks6d1c6lem4  42667  aks6d1c6isolem1  42668  aks5lem3a  42683  grpods  42688  unitscyglem1  42689  unitscyglem2  42690  ofun  42731  redivcan2d  42933  redivcan3d  42934  sn-rediv0d  42939  sn-redividd  42940  rhmpsr1  43043  evlselv  43048  fsuppind  43049  mhphf  43056  3cubeslem3r  43145  eldiophb  43215  eldioph  43216  eldioph3  43224  rabren3dioph  43269  pellqrexplicit  43331  rmxycomplete  43371  rmxynorm  43372  acongrep  43434  jm2.26a  43454  jm2.26  43456  fnwe2lem2  43505  fnwe2lem3  43506  aomclem5  43512  aomclem8  43515  imasgim  43554  isnumbasgrplem1  43555  hbtlem5  43582  dgrsub2  43589  rgspnid  43622  rngunsnply  43623  mendval  43633  mendring  43642  mendlmod  43643  mendassa  43644  nnoeomeqom  43766  tfsconcatb0  43798  oaun3  43836  safesnsupfilb  43871  fsovrfovd  44462  fsovcnvlem  44466  mnring0gd  44674  mnringlmodd  44679  mnringmulrcld  44681  colleq1  44707  colleq2  44708  dvgrat  44765  radcnvrat  44767  hashnzfzclim  44775  caofcan  44776  ofsubid  44777  ofmul12  44778  ofdivrec  44779  ofdivcan4  44780  ofdivdiv2  44781  expgrowth  44788  binomcxplemnn0  44802  binomcxplemrat  44803  binomcxplemdvbinom  44806  binomcxplemnotnn0  44809  wessf1ornlem  45640  disjf1o  45646  ssnnf1octb  45649  mapss2  45659  icof  45672  mpteq1df  45688  infnsuprnmpt  45702  upbdrech  45761  divcan8d  45768  dmmcand  45769  suplesup  45792  ssuzfz  45802  supsubc  45806  xralrple2  45807  fprodabs2  46048  fprodcn  46053  clim1fr1  46054  climrec  46056  climexp  46058  climinf  46059  climsuse  46061  climneg  46063  divcnvg  46080  sumnnodd  46083  clim2f  46087  clim2f2  46121  fnlimfvre  46125  climleltrp  46127  climreclmpt  46135  climinf2mpt  46165  climinfmpt  46166  supcnvlimsup  46191  climuzlem  46194  climisp  46197  climrescn  46199  climxrrelem  46200  climxrre  46201  liminfvalxrmpt  46237  liminflbuz2  46266  cncfcompt  46334  dvsinax  46364  fperdvper  46370  dvcosax  46377  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  dvnxpaek  46393  dvnmul  46394  dvmptfprodlem  46395  dvnprodlem1  46397  dvnprodlem2  46398  dvnprodlem3  46399  iblempty  46416  iblsplit  46417  itgcoscmulx  46420  itgsincmulx  46425  itgsubsticc  46427  sublevolico  46435  stoweidlem2  46453  stoweidlem17  46468  stoweidlem21  46472  stoweidlem32  46483  stoweidlem46  46497  stoweidlem55  46506  wallispi  46521  wallispi2lem1  46522  wallispi2lem2  46523  wallispi2  46524  stirlinglem3  46527  dirkercncflem2  46555  dirkercncflem4  46557  fourierdlem16  46574  fourierdlem18  46576  fourierdlem21  46579  fourierdlem22  46580  fourierdlem39  46597  fourierdlem53  46610  fourierdlem58  46615  fourierdlem59  46616  fourierdlem62  46619  fourierdlem73  46630  fourierdlem76  46633  fourierdlem81  46638  fourierdlem83  46640  fourierdlem93  46650  fourierdlem101  46658  fourierdlem103  46660  fourierdlem104  46661  fourierdlem111  46668  fourierdlem112  46669  fouriersw  46682  elaa2lem  46684  etransclem18  46703  etransclem32  46717  etransclem33  46718  etransclem46  46731  etransclem48  46733  rrxtopnfi  46738  rrxunitopnfi  46743  salincl  46775  sge0z  46826  sge0tsms  46831  sge0snmpt  46834  sge0sup  46842  sge0resplit  46857  sge0ss  46863  sge0isum  46878  sge0xp  46880  sge0xaddlem2  46885  sge0seq  46897  sge0reuzb  46899  meadjun  46913  meadjiun  46917  ismeannd  46918  meaiunlelem  46919  meaiininclem  46937  caragenunidm  46959  caragenuncllem  46963  omeiunltfirp  46970  carageniuncllem1  46972  caratheodorylem1  46977  0ome  46980  isomenndlem  46981  hoicvr  46999  hoicvrrex  47007  ovn0lem  47016  ovn0  47017  ovnsubaddlem1  47021  hoidmvval0  47038  hoidmvval0b  47041  hoidmv1lelem1  47042  hoidmv1le  47045  hoidmvlelem2  47047  hoidmvlelem3  47048  hoidmvlelem4  47049  hoidmvlelem5  47050  ovnhoilem1  47052  ovnhoilem2  47053  ovnhoi  47054  dmvon  47057  hspval  47060  ovnlecvr2  47061  hoiqssbllem2  47074  hspmbllem2  47078  hspmbl  47080  hoimbl  47082  ovnsubadd2lem  47096  ovolval4lem1  47100  ovnovollem1  47107  vonvolmbl  47112  vonvol2  47115  iccvonmbllem  47129  vonioolem2  47132  vonn0ioo2  47141  vonn0icc2  47143  smfpimltmpt  47197  issmfdmpt  47199  smfconst  47200  smfpimltxrmptf  47209  smflimlem2  47223  smflimlem3  47224  smflim  47228  smfpimgtmpt  47232  smfpimgtxrmptf  47235  smfsupmpt  47266  smfinfmpt  47270  smflimsuplem4  47274  fresfo  47519  fsetsnf  47522  fsetsnprcnex  47526  cfsetsnfsetf  47529  cfsetsnfsetfo  47531  3f1oss1  47546  f1cof1b  47548  funfocofob  47549  afveq1  47605  afveq2  47606  afvco2  47647  rspceaov  47668  faovcl  47671  afv2eq12d  47686  afv2eq1  47687  afv2eq2  47688  dfatcolem  47726  f1oresf1orab  47760  preimafvsnel  47862  preimafvelsetpreimafv  47871  fundcmpsurbijinjpreimafv  47890  fundcmpsurinjimaid  47894  fundcmpsurinjALT  47895  ichnreuop  47955  ichreuopeq  47956  prelspr  47969  sprsymrelf1lem  47974  sprsymrelfolem2  47976  prproropreud  47992  reuopreuprim  48009  fmtnofac2lem  48054  proththd  48100  requad01  48120  dfodd6  48136  nnsum3primesprm  48289  clnbgrvtxel  48328  isgrim  48381  grimid  48385  upgrimtrls  48405  isubgrgrim  48428  clnbgrgrim  48433  usgrgrtrirex  48449  stgrnbgr0  48463  isubgr3stgrlem6  48470  isgrlim  48481  uspgrlim  48491  grlimedgclnbgr  48494  grlimgrtri  48502  grilcbri2  48510  gpgedgiov  48564  gpg5gricstgr3  48589  gpg5grlim  48592  grlimedgnedg  48630  uspgrsprfo  48647  copissgrp  48667  copisnmnd  48668  isasslaw  48691  2zrngamgm  48744  cznrng  48760  rngcvalALTV  48764  rngcbasALTV  48765  rngchomfvalALTV  48766  rngccofvalALTV  48769  rngccoALTV  48770  rngccatidALTV  48771  rhmsubcALTV  48784  ringcvalALTV  48788  ringcbasALTV  48799  ringchomfvalALTV  48800  ringccofvalALTV  48803  ringccoALTV  48804  ringccatidALTV  48805  scmsuppss  48870  ply1mulgsum  48889  dflinc2  48909  lcoop  48910  lincvalsng  48915  lincvalpr  48917  lincvalsc0  48920  lcoc0  48921  lcoel0  48927  lincsum  48928  lincolss  48933  islininds  48945  lindslinindsimp1  48956  lindsrng01  48967  snlindsntorlem  48969  lincresunit3  48980  islindeps2  48982  lmod1lem3  48988  lmod1zr  48992  itcoval  49160  itcoval0  49161  itcoval1  49162  itcoval2  49163  itcoval3  49164  itcovalsuc  49166  itcovalsucov  49167  itcovalendof  49168  itcovalpclem2  49170  itcovalt2lem2  49175  ackvalsuc1mpt  49177  ackval1  49180  ackval2  49181  ackval3  49182  ackvalsucsucval  49187  affinecomb1  49201  rrx2plordisom  49222  lines  49230  line  49231  rrxline  49233  spheres  49245  line2xlem  49252  itsclc0yqsol  49263  itscnhlinecirc02p  49284  fmpod  49368  iscnrm3llem1  49447  iscnrm3llem2  49448  iscnrm3l  49449  glbsscl  49459  posjidm  49470  posmidm  49471  toslat  49480  ipolubdm  49485  ipoglbdm  49488  mreclat  49495  topclat  49496  iinfssc  49555  iinfsubc  49556  infsubc2  49559  iinfconstbas  49564  nelsubc3  49569  initc  49589  funchomf  49595  imaidfu2lem  49607  imaidfu  49608  imaidfu2  49609  cofidf2  49618  funcoppc4  49642  fthcomf  49655  idfth  49656  idsubc  49658  upciclem1  49664  upfval2  49675  upfval3  49676  isuplem  49677  oppcup3lem  49704  uobffth  49716  uobeqw  49717  uptr2  49719  initopropd  49741  termopropd  49742  dfswapf2  49759  swapfelvv  49761  swapf1vala  49764  swapf2fn  49766  swapf2  49772  tposcurf1cl  49794  tposcurf11  49795  tposcurf12  49796  tposcurf1  49797  tposcurf2  49798  tposcurf2val  49799  tposcurf2cl  49800  tposcurfcl  49801  fucoelvv  49818  fucofvalne  49823  fuco11  49824  fuco11cl  49825  fuco21  49834  fuco11b  49835  fuco11bALT  49836  fuco22natlem3  49842  fuco22natlem  49843  fuco23a  49850  fucofunc  49857  fucofunca  49858  fucolid  49859  fucorid  49860  postcofval  49862  precofval  49865  precofvalALT  49866  precoffunc  49870  prcofelvv  49878  reldmprcof1  49879  reldmprcof2  49880  prcoftposcurfuco  49881  prcoffunc  49883  prcoffunca  49884  fucoppcco  49907  fucoppccic  49911  oppfdiag1  49912  oppfdiag1a  49913  isthincd2lem1  49923  oppcthin  49936  oppcthinco  49937  subthinc  49941  fullthinc  49948  thincciso2  49953  indthinc  49960  prsthinc  49962  setcthin  49963  setc2othin  49964  setcsnterm  49988  setc1ocofval  49992  isinito2lem  49996  dfinito4  49999  idfudiag1  50023  arweuthinc  50027  diag1f1olem  50031  prstchomval  50057  prstcprs  50058  prstcthin  50059  prstchom2  50061  oduoppcciso  50064  postcpos  50065  postcposALT  50066  postc  50067  mndtccatid  50085  mndtcid  50087  oppgoppchom  50088  oppgoppcco  50089  oppgoppcid  50090  grptcmon  50091  grptcepi  50092  2arwcat  50098  lanfval  50111  ranfval  50112  lanpropd  50113  ranpropd  50114  rellan  50121  lanrcl5  50133  ranrcl5  50138  lanup  50139  ranup  50140  lmdfval  50147  cmdfval  50148  lmdpropd  50155  cmdpropd  50156  concom  50161  coccom  50162  islmd  50163  iscmd  50164  lmddu  50165  termolmd  50168  lmdran  50169  cmdlan  50170  aacllem  50299  amgmwlem  50300