Theorem mgpbas 19992

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 2732	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 19989	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17146	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17226	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19213	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2760	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1541  ‘cfv 6543  Basecbs 17143  ._rcmulr 17197  mulGrpcmgp 19986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-nn 12212  df-2 12274  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-plusg 17209  df-mgp 19987

This theorem is referenced by:  mgptopn  19998  mgpress  20001  mgpressOLD  20002  dfur2  20006  srgcl  20015  srgass  20016  srgideu  20017  srgidcl  20021  srgidmlem  20023  issrgid  20026  srg1zr  20037  srgpcomp  20040  srgpcompp  20041  srgpcomppsc  20042  srgbinomlem1  20048  srgbinomlem4  20051  srgbinomlem  20052  srgbinom  20053  csrgbinom  20054  ringcl  20072  crngcom  20073  iscrng2  20074  ringass  20075  ringideu  20076  crngbascntr  20077  ringidcl  20082  ringidmlem  20084  isringid  20087  ringidss  20093  ringpropd  20101  crngpropd  20102  isringd  20104  iscrngd  20105  ring1  20121  gsummgp0  20129  prdsmgp  20131  pwspjmhmmgpd  20140  pwsexpg  20141  xpsring1d  20145  oppr1  20163  unitgrpbas  20195  unitsubm  20199  rngidpropd  20228  dfrhm2  20252  rhmmul  20263  isrhm2d  20264  idrhm  20267  rhmf1o  20268  pwsco1rhm  20276  pwsco2rhm  20277  subrgsubm  20331  issubrg3  20346  cntzsubr  20352  pwsdiagrhm  20353  rhmpropd  20355  isdrng2  20370  drngmcl  20373  drngid2  20377  isdrngd  20389  isdrngdOLD  20391  subrgacs  20415  cntzsdrg  20417  subdrgint  20418  primefld  20420  rlmscaf  20830  xrsmcmn  20967  cnfldexp  20977  cnmsubglem  21007  expmhm  21013  nn0srg  21014  rge0srg  21015  expghm  21044  cnmsgnbas  21130  sraassab  21421  sraassaOLD  21423  assamulgscmlem1  21452  assamulgscmlem2  21453  psrcrng  21532  mplcoe3  21592  mplcoe5lem  21593  mplcoe5  21594  mplbas2  21596  evlslem3  21642  evlslem6  21643  evlslem1  21644  evlsgsummul  21654  evlspw  21655  mpfind  21669  mhppwdeg  21692  ply1moncl  21792  coe1tm  21794  coe1pwmul  21800  ply1scltm  21802  ply1coefsupp  21818  ply1coe  21819  gsummoncoe1  21827  lply1binomsc  21830  evls1gsummul  21843  evls1pw  21844  evl1expd  21863  evl1gsummul  21878  evl1scvarpw  21881  evl1scvarpwval  21882  evl1gsummon  21883  ringvcl  21899  mamuvs2  21905  matgsumcl  21961  madetsmelbas  21965  madetsmelbas2  21966  mat1mhm  21985  scmatmhm  22035  mdetleib2  22089  mdetf  22096  m1detdiag  22098  mdetdiaglem  22099  mdetdiag  22100  mdetdiagid  22101  mdetrlin  22103  mdetrsca  22104  mdetralt  22109  mdetunilem7  22119  mdetunilem8  22120  mdetuni0  22122  m2detleiblem2  22129  m2detleiblem3  22130  m2detleiblem4  22131  smadiadetlem4  22170  mat2pmatmhm  22234  pmatcollpwscmatlem1  22290  mply1topmatcllem  22304  mply1topmatcl  22306  pm2mpghm  22317  pm2mpmhm  22321  monmat2matmon  22325  pm2mp  22326  chpscmat  22343  chpscmatgsumbin  22345  chpscmatgsummon  22346  chp0mat  22347  chpidmat  22348  chfacfscmulcl  22358  chfacfscmul0  22359  chfacfscmulgsum  22361  chfacfpmmulcl  22362  chfacfpmmul0  22363  chfacfpmmulgsum  22365  chfacfpmmulgsum2  22366  cayhamlem1  22367  cpmadugsumlemB  22375  cpmadugsumlemC  22376  cpmadugsumlemF  22377  cayhamlem2  22385  cayhamlem4  22389  nrgtrg  24206  deg1pw  25637  ply1remlem  25679  fta1blem  25685  plypf1  25725  efabl  26058  efsubm  26059  amgm  26492  wilthlem2  26570  wilthlem3  26571  dchrelbas2  26737  dchrelbas3  26738  dchrzrhmul  26746  dchrmulcl  26749  dchrn0  26750  dchrinvcl  26753  dchrfi  26755  dchrsum2  26768  sum2dchr  26774  lgsqrlem1  26846  lgsqrlem2  26847  lgsqrlem3  26848  lgsqrlem4  26849  lgseisenlem3  26877  lgseisenlem4  26878  dchrisum0flblem1  27008  cntrcrng  32209  psgnid  32251  cnmsgn0g  32300  altgnsg  32303  urpropd  32373  freshmansdream  32376  frobrhm  32377  fermltlchr  32473  znfermltl  32474  elringlsm  32498  ringlsmss  32500  lsmsnpridl  32503  cringm4  32560  mxidlprm  32581  evls1fpws  32641  ply1fermltlchr  32657  gsummoncoe1fzo  32663  ply1degltdimlem  32702  ply1degltdim  32703  mdetpmtr1  32798  iistmd  32877  xrge0iifmhm  32914  xrge0pluscn  32915  pl1cn  32930  pwsgprod  41116  evlsvvvallem  41135  evlsvvval  41137  evlsexpval  41141  selvvvval  41159  evlselv  41161  mhphf  41171  hbtlem4  41858  idomrootle  41927  isdomn3  41936  mon1psubm  41938  deg1mhm  41939  amgm2d  42940  amgm3d  42941  amgm4d  42942  isringrng  46647  rngass  46648  rngcl  46653  isrngd  46662  rngpropd  46663  isrnghmmul  46681  rnghmf1o  46691  idrnghm  46697  c0rhm  46701  c0rnghm  46702  rhmimasubrnglem  46734  rhmimasubrng  46735  cntzsubrng  46736  rnglidlmmgm  46746  rnglidlmsgrp  46747  rng2idl1cntr  46780  2zrngmmgm  46834  2zrngmsgrp  46835  2zrngnring  46840  cznrng  46843  cznnring  46844  mgpsumunsn  47027  mgpsumz  47028  mgpsumn  47029  invginvrid  47033  ply1vr1smo  47052  ply1mulgsumlem4  47060  ply1mulgsum  47061  amgmlemALT  47840  amgmw2d  47841