Theorem mgpbas 19987

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

Syntax hints:   = wceq 1541  ‘cfv 6540  Basecbs 17140  ._rcmulr 17194  mulGrpcmgp 19981

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 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

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 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-plusg 17206  df-mgp 19982

This theorem is referenced by:  mgptopn  19993  mgpress  19996  mgpressOLD  19997  dfur2  20001  srgcl  20009  srgass  20010  srgideu  20011  srgidcl  20015  srgidmlem  20017  issrgid  20020  srg1zr  20031  srgpcomp  20034  srgpcompp  20035  srgpcomppsc  20036  srgbinomlem1  20042  srgbinomlem4  20045  srgbinomlem  20046  srgbinom  20047  csrgbinom  20048  ringcl  20066  crngcom  20067  iscrng2  20068  ringass  20069  ringideu  20070  crngbascntr  20071  ringidcl  20076  ringidmlem  20078  isringid  20081  ringidss  20087  ringpropd  20095  crngpropd  20096  isringd  20098  iscrngd  20099  ring1  20115  gsummgp0  20123  prdsmgp  20125  pwspjmhmmgpd  20134  pwsexpg  20135  oppr1  20156  unitgrpbas  20188  unitsubm  20192  rngidpropd  20221  dfrhm2  20245  rhmmul  20256  isrhm2d  20257  idrhm  20260  rhmf1o  20261  pwsco1rhm  20269  pwsco2rhm  20270  isdrng2  20321  drngmcl  20324  drngid2  20328  isdrngd  20340  isdrngdOLD  20342  subrgsubm  20368  issubrg3  20384  cntzsubr  20390  pwsdiagrhm  20391  rhmpropd  20393  subrgacs  20408  cntzsdrg  20410  subdrgint  20411  primefld  20413  rlmscaf  20823  xrsmcmn  20960  cnfldexp  20970  cnmsubglem  21000  expmhm  21006  nn0srg  21007  rge0srg  21008  expghm  21036  cnmsgnbas  21122  sraassab  21413  sraassaOLD  21415  assamulgscmlem1  21444  assamulgscmlem2  21445  psrcrng  21524  mplcoe3  21584  mplcoe5lem  21585  mplcoe5  21586  mplbas2  21588  evlslem3  21634  evlslem6  21635  evlslem1  21636  evlsgsummul  21646  evlspw  21647  mpfind  21661  mhppwdeg  21684  ply1moncl  21784  coe1tm  21786  coe1pwmul  21792  ply1scltm  21794  ply1coefsupp  21810  ply1coe  21811  gsummoncoe1  21819  lply1binomsc  21822  evls1gsummul  21835  evls1pw  21836  evl1expd  21855  evl1gsummul  21870  evl1scvarpw  21873  evl1scvarpwval  21874  evl1gsummon  21875  ringvcl  21891  mamuvs2  21897  matgsumcl  21953  madetsmelbas  21957  madetsmelbas2  21958  mat1mhm  21977  scmatmhm  22027  mdetleib2  22081  mdetf  22088  m1detdiag  22090  mdetdiaglem  22091  mdetdiag  22092  mdetdiagid  22093  mdetrlin  22095  mdetrsca  22096  mdetralt  22101  mdetunilem7  22111  mdetunilem8  22112  mdetuni0  22114  m2detleiblem2  22121  m2detleiblem3  22122  m2detleiblem4  22123  smadiadetlem4  22162  mat2pmatmhm  22226  pmatcollpwscmatlem1  22282  mply1topmatcllem  22296  mply1topmatcl  22298  pm2mpghm  22309  pm2mpmhm  22313  monmat2matmon  22317  pm2mp  22318  chpscmat  22335  chpscmatgsumbin  22337  chpscmatgsummon  22338  chp0mat  22339  chpidmat  22340  chfacfscmulcl  22350  chfacfscmul0  22351  chfacfscmulgsum  22353  chfacfpmmulcl  22354  chfacfpmmul0  22355  chfacfpmmulgsum  22357  chfacfpmmulgsum2  22358  cayhamlem1  22359  cpmadugsumlemB  22367  cpmadugsumlemC  22368  cpmadugsumlemF  22369  cayhamlem2  22377  cayhamlem4  22381  nrgtrg  24198  deg1pw  25629  ply1remlem  25671  fta1blem  25677  plypf1  25717  efabl  26050  efsubm  26051  amgm  26484  wilthlem2  26562  wilthlem3  26563  dchrelbas2  26729  dchrelbas3  26730  dchrzrhmul  26738  dchrmulcl  26741  dchrn0  26742  dchrinvcl  26745  dchrfi  26747  dchrsum2  26760  sum2dchr  26766  lgsqrlem1  26838  lgsqrlem2  26839  lgsqrlem3  26840  lgsqrlem4  26841  lgseisenlem3  26869  lgseisenlem4  26870  dchrisum0flblem1  27000  cntrcrng  32201  psgnid  32243  cnmsgn0g  32292  altgnsg  32295  urpropd  32365  freshmansdream  32369  frobrhm  32370  fermltlchr  32466  znfermltl  32467  elringlsm  32491  ringlsmss  32493  lsmsnpridl  32496  cringm4  32553  mxidlprm  32574  evls1fpws  32634  ply1fermltlchr  32650  gsummoncoe1fzo  32656  ply1degltdimlem  32695  ply1degltdim  32696  mdetpmtr1  32791  iistmd  32870  xrge0iifmhm  32907  xrge0pluscn  32908  pl1cn  32923  pwsgprod  41111  evlsvvvallem  41130  evlsvvval  41132  evlsexpval  41136  selvvvval  41154  evlselv  41156  mhphf  41166  hbtlem4  41853  idomrootle  41922  isdomn3  41931  mon1psubm  41933  deg1mhm  41934  amgm2d  42935  amgm3d  42936  amgm4d  42937  isringrng  46643  rngass  46644  rngcl  46649  isrngd  46658  rngpropd  46659  isrnghmmul  46676  rnghmf1o  46686  idrnghm  46692  c0rhm  46696  c0rnghm  46697  rhmimasubrnglem  46728  rhmimasubrng  46729  cntzsubrng  46730  rnglidlmmgm  46738  rnglidlmsgrp  46739  rng2idl1cntr  46770  2zrngmmgm  46797  2zrngmsgrp  46798  2zrngnring  46803  cznrng  46806  cznnring  46807  mgpsumunsn  46990  mgpsumz  46991  mgpsumn  46992  invginvrid  46996  ply1vr1smo  47015  ply1mulgsumlem4  47023  ply1mulgsum  47024  amgmlemALT  47803  amgmw2d  47804