Theorem mgpbas 20371

Description: Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)

Hypotheses

Ref	Expression
mgpbas.1	⊢ 𝑀 = (mulGrp‘𝑅)
mgpbas.2	⊢ 𝐵 = (Base‘𝑅)

Assertion

Ref	Expression
mgpbas	⊢ 𝐵 = (Base‘𝑀)

Proof of Theorem mgpbas

Step	Hyp	Ref	Expression
1		mgpbas.2	. 2 ⊢ 𝐵 = (Base‘𝑅)
2		mgpbas.1	. . . 4 ⊢ 𝑀 = (mulGrp‘𝑅)
3		eqid 2760	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20369	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17396	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17464	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19570	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2783	1 ⊢ 𝐵 = (Base‘𝑀)

This proof depends on syntax axioms:   = wceq 1569  ‘cfv 6539  Basecbs 17393  ._rcmulr 17435  mulGrpcmgp 20366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-nn 12340  df-2 12409  df-sets 17348  df-slot 17366  df-ndx 17378  df-base 17394  df-plusg 17447  df-mgp 20367

This theorem is used by:  mgptopn  20374  mgpress  20376  prdsmgp  20377  elmgplsm  20378  rngass  20387  rngcl  20392  isrngd  20401  rngpropd  20402  rng1zrlem  20409  dfur2  20416  srgcl  20425  srgass  20426  srgideu  20427  srgidcl  20431  srgidmlem  20433  issrgid  20436  srgpcomp  20450  srgpcompp  20451  srgpcomppsc  20452  srgbinomlem1  20458  srgbinomlem4  20461  srgbinomlem  20462  srgbinom  20463  csrgbinom  20464  ringcl  20483  crngcom  20484  iscrng2  20485  ringass  20486  ringideu  20487  crngbascntr  20489  ringidcl  20500  ringidmlem  20503  isringid  20506  ringidss  20512  isringrng  20522  dfring3  20524  ringpropd  20525  crngpropd  20526  isringd  20528  iscrngd  20529  ring1  20547  gsummgp0  20553  pwspjmhmmgpd  20563  pwsexpg  20564  pwsgprod  20565  xpsring1d  20569  oppr1  20586  unitgrpbas  20618  unitsubm  20622  rngidpropd  20651  isrnghmmul  20678  rnghmf1o  20688  idrnghm  20694  dfrhm2  20710  rhmmul  20726  isrhm2d  20727  idrhm  20731  rhmf1o  20733  pwsco1rhm  20747  pwsco2rhm  20748  c0rhm  20792  c0rnghm  20793  rhmimasubrnglem  20823  rhmimasubrng  20824  cntzsubrng  20825  subrgsubm  20843  issubrg3  20858  cntzsubr  20864  pwsdiagrhm  20865  rhmpropd  20867  isdomn3  20972  isdrng2  21003  isdrng3lem0  21010  isdrng3lem1  21011  drngid2  21016  isdrngd  21028  isdrngdOLD  21030  subrgacs  21063  cntzsdrg  21065  subdrgint  21066  primefld  21068  rlmscaf  21488  rnglidlmmgm  21539  rnglidlmsgrp  21540  rng2idl1cntr  21607  cringm4  21633  ssdifidlprm  21648  prmidlsubm  21649  xrsmcmn  21707  cnfldexp  21717  cnmsubglem  21742  expmhm  21748  nn0srg  21749  rge0srg  21750  expghm  21787  fermltlchr  21841  freshmansdream  21886  frobrhm  21887  cnmsgnbas  21890  sraassab  22182  assamulgscmlem1  22213  assamulgscmlem2  22214  psrcrng  22285  mplcoe3  22353  mplcoe5lem  22354  mplcoe5  22355  mplbas2  22357  evlslem3  22395  evlslem6  22396  evlslem1  22397  evlsvvvallem  22406  evlsvvval  22408  evlsgsummul  22412  evlspw  22413  mpfind  22430  evlsexpval  22443  selvvvval  22457  mhppwdeg  22477  psdpw  22497  ply1moncl  22596  coe1tm  22598  coe1pwmul  22604  ply1scltm  22606  ply1idvr1  22619  ply1coefsupp  22621  ply1coe  22622  gsummoncoe1  22632  lply1binomsc  22635  ply1fermltlchr  22636  evls1gsummul  22649  evls1pw  22650  evl1expd  22669  evl1gsummul  22684  evl1scvarpw  22687  evl1scvarpwval  22688  evl1gsummon  22689  evls1fpws  22693  rhmply1mon  22710  ringvcl  22721  mamuvs2  22727  matgsumcl  22781  madetsmelbas  22785  madetsmelbas2  22786  mat1mhm  22805  scmatmhm  22855  mdetleib2  22909  mdetf  22916  m1detdiag  22918  mdetdiaglem  22919  mdetdiag  22920  mdetdiagid  22921  mdetrlin  22923  mdetrsca  22924  mdetralt  22929  mdetunilem7  22939  mdetunilem8  22940  mdetuni0  22942  m2detleiblem2  22949  m2detleiblem3  22950  m2detleiblem4  22951  smadiadetlem4  22990  mat2pmatmhm  23057  pmatcollpwscmatlem1  23113  mply1topmatcllem  23127  mply1topmatcl  23129  pm2mpghm  23140  pm2mpmhm  23144  monmat2matmon  23148  pm2mp  23149  chpscmat  23166  chpscmatgsumbin  23168  chpscmatgsummon  23169  chp0mat  23170  chpidmat  23171  chfacfscmulcl  23181  chfacfscmul0  23182  chfacfscmulgsum  23184  chfacfpmmulcl  23185  chfacfpmmul0  23186  chfacfpmmulgsum  23188  chfacfpmmulgsum2  23189  cayhamlem1  23190  cpmadugsumlemB  23198  cpmadugsumlemC  23199  cpmadugsumlemF  23200  cayhamlem2  23208  cayhamlem4  23212  nrgtrg  25015  deg1pw  26445  ply1remlem  26489  fta1blem  26495  idomrootle  26497  plypf1  26537  efabl  26884  efsubm  26885  amgm  27324  wilthlem2  27402  wilthlem3  27403  dchrelbas2  27570  dchrelbas3  27571  dchrzrhmul  27579  dchrmulcl  27582  dchrn0  27583  dchrinvcl  27586  dchrfi  27588  dchrsum2  27601  sum2dchr  27607  lgsqrlem1  27679  lgsqrlem2  27680  lgsqrlem3  27681  lgsqrlem4  27682  lgseisenlem3  27710  lgseisenlem4  27711  dchrisum0flblem1  27841  zsoring  28801  cntrcrng  33689  psgnid  33705  cnmsgn0g  33754  altgnsg  33757  urpropd  33838  ringm1expp1  33841  isunit3  33848  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem3  33852  elrgspnlem4  33853  elrgspn  33854  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  0ringcring  33860  erlbr2d  33872  erler  33873  erld2  33874  rlocaddval  33877  rlocmulval  33878  rloccring  33879  rloc0g  33880  rloc1r  33881  rlocf1  33882  rlocinvunit  33883  rlocisunit  33884  domnprodn0  33886  domnprodeq0  33887  rrgsubm  33892  znfermltl  33969  unitprodclb  33991  ringlsmss  33995  lsmsnpridl  33998  mxidlprm  34042  rprmdvdspow  34112  rprmdvdsprod  34113  1arithidomlem1  34114  1arithidom  34116  1arithufdlem1  34123  1arithufdlem2  34124  1arithufdlem3  34125  1arithufdlem4  34126  dfufd2lem  34128  zringfrac  34133  ressply1evls1  34144  evl1deg1  34155  evl1deg2  34156  evl1deg3  34157  evls1monply1  34158  deg1prod  34162  ply1coedeg  34168  coe1vr1  34170  deg1vr  34171  gsummoncoe1fzo  34176  evlextv  34221  psrmonprod  34231  mplmonprod  34233  vietalem  34258  vieta  34259  srapwov  34268  ply1degltdimlem  34301  ply1degltdim  34302  assarrginv  34315  evls1fldgencl  34349  extdgfialglem1  34371  extdgfialglem2  34372  rtelextdg2lem  34405  2sqr3minply  34459  cos9thpiminplylem6  34466  cos9thpiminply  34467  mdetpmtr1  34502  iistmd  34581  xrge0iifmhm  34618  xrge0pluscn  34619  pl1cn  34634  zrhcntr  34658  aks6d1c1p2  43253  aks6d1c1p3  43254  aks6d1c1p4  43255  aks6d1c1p5  43256  aks6d1c1p7  43257  aks6d1c1p6  43258  aks6d1c1p8  43259  aks6d1c1  43260  evl1gprodd  43261  aks6d1c2lem4  43271  idomnnzpownz  43276  idomnnzgmulnz  43277  ringexp0nn  43278  aks6d1c5lem0  43279  aks6d1c5lem3  43281  aks6d1c5lem2  43282  aks6d1c5  43283  deg1gprod  43284  deg1pow  43285  aks6d1c6lem1  43314  aks6d1c6lem2  43315  aks6d1c6lem3  43316  aks5lem2  43331  aks5lem3a  43333  unitscyglem5  43343  aks5lem7  43344  domnexpgn0cl  43678  abvexp  43690  fidomncyc  43693  evlselv  43711  mhphf  43719  hbtlem4  44222  mon1psubm  44295  deg1mhm  44296  amgm2d  45292  amgm3d  45293  amgm4d  45294  2zrngmmgm  49443  2zrngmsgrp  49444  2zrngnring  49449  cznrng  49452  cznnring  49453  mgpsumunsn  49567  mgpsumz  49568  mgpsumn  49569  invginvrid  49573  ply1vr1smo  49589  ply1mulgsumlem4  49595  ply1mulgsum  49596  elmgpcntrd  50213  amgmlemALT  51157  amgmw2d  51158