Theorem mgpbas 20048

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 2729	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20046	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17141	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17209	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19247	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2752	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1540  ‘cfv 6486  Basecbs 17138  ._rcmulr 17180  mulGrpcmgp 20043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-nn 12147  df-2 12209  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17139  df-plusg 17192  df-mgp 20044

This theorem is referenced by:  mgptopn  20051  mgpress  20053  prdsmgp  20054  rngass  20062  rngcl  20067  isrngd  20076  rngpropd  20077  dfur2  20087  srgcl  20096  srgass  20097  srgideu  20098  srgidcl  20102  srgidmlem  20104  issrgid  20107  srg1zr  20118  srgpcomp  20121  srgpcompp  20122  srgpcomppsc  20123  srgbinomlem1  20129  srgbinomlem4  20132  srgbinomlem  20133  srgbinom  20134  csrgbinom  20135  ringcl  20153  crngcom  20154  iscrng2  20155  ringass  20156  ringideu  20157  crngbascntr  20159  ringidcl  20168  ringidmlem  20171  isringid  20174  ringidss  20180  isringrng  20190  ringpropd  20191  crngpropd  20192  isringd  20194  iscrngd  20195  ring1  20213  gsummgp0  20221  pwspjmhmmgpd  20231  pwsexpg  20232  xpsring1d  20236  oppr1  20253  unitgrpbas  20285  unitsubm  20289  rngidpropd  20318  isrnghmmul  20345  rnghmf1o  20355  idrnghm  20361  dfrhm2  20377  rhmmul  20389  isrhm2d  20390  idrhm  20393  rhmf1o  20394  pwsco1rhm  20405  pwsco2rhm  20406  c0rhm  20437  c0rnghm  20438  rhmimasubrnglem  20468  rhmimasubrng  20469  cntzsubrng  20470  subrgsubm  20488  issubrg3  20503  cntzsubr  20509  pwsdiagrhm  20510  rhmpropd  20512  isdomn3  20618  isdrng2  20646  drngmclOLD  20654  drngid2  20655  isdrngd  20668  isdrngdOLD  20670  subrgacs  20703  cntzsdrg  20705  subdrgint  20706  primefld  20708  rlmscaf  21129  rnglidlmmgm  21170  rnglidlmsgrp  21171  rng2idl1cntr  21230  xrsmcmn  21316  cnfldexp  21329  cnmsubglem  21355  expmhm  21361  nn0srg  21362  rge0srg  21363  expghm  21400  fermltlchr  21454  freshmansdream  21499  frobrhm  21500  cnmsgnbas  21503  sraassab  21793  sraassaOLD  21795  assamulgscmlem1  21824  assamulgscmlem2  21825  psrcrng  21897  mplcoe3  21961  mplcoe5lem  21962  mplcoe5  21963  mplbas2  21965  evlslem3  22003  evlslem6  22004  evlslem1  22005  evlsgsummul  22015  evlspw  22016  mpfind  22030  mhppwdeg  22053  psdpw  22073  ply1moncl  22173  coe1tm  22175  coe1pwmul  22181  ply1scltm  22183  ply1idvr1  22197  ply1coefsupp  22200  ply1coe  22201  gsummoncoe1  22211  lply1binomsc  22214  ply1fermltlchr  22215  evls1gsummul  22228  evls1pw  22229  evl1expd  22248  evl1gsummul  22263  evl1scvarpw  22266  evl1scvarpwval  22267  evl1gsummon  22268  evls1fpws  22272  rhmply1mon  22292  ringvcl  22303  mamuvs2  22309  matgsumcl  22363  madetsmelbas  22367  madetsmelbas2  22368  mat1mhm  22387  scmatmhm  22437  mdetleib2  22491  mdetf  22498  m1detdiag  22500  mdetdiaglem  22501  mdetdiag  22502  mdetdiagid  22503  mdetrlin  22505  mdetrsca  22506  mdetralt  22511  mdetunilem7  22521  mdetunilem8  22522  mdetuni0  22524  m2detleiblem2  22531  m2detleiblem3  22532  m2detleiblem4  22533  smadiadetlem4  22572  mat2pmatmhm  22636  pmatcollpwscmatlem1  22692  mply1topmatcllem  22706  mply1topmatcl  22708  pm2mpghm  22719  pm2mpmhm  22723  monmat2matmon  22727  pm2mp  22728  chpscmat  22745  chpscmatgsumbin  22747  chpscmatgsummon  22748  chp0mat  22749  chpidmat  22750  chfacfscmulcl  22760  chfacfscmul0  22761  chfacfscmulgsum  22763  chfacfpmmulcl  22764  chfacfpmmul0  22765  chfacfpmmulgsum  22767  chfacfpmmulgsum2  22768  cayhamlem1  22769  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  cayhamlem2  22787  cayhamlem4  22791  nrgtrg  24594  deg1pw  26042  ply1remlem  26086  fta1blem  26092  idomrootle  26094  plypf1  26133  efabl  26475  efsubm  26476  amgm  26917  wilthlem2  26995  wilthlem3  26996  dchrelbas2  27164  dchrelbas3  27165  dchrzrhmul  27173  dchrmulcl  27176  dchrn0  27177  dchrinvcl  27180  dchrfi  27182  dchrsum2  27195  sum2dchr  27201  lgsqrlem1  27273  lgsqrlem2  27274  lgsqrlem3  27275  lgsqrlem4  27276  lgseisenlem3  27304  lgseisenlem4  27305  dchrisum0flblem1  27435  zsoring  28319  cntrcrng  33036  psgnid  33052  cnmsgn0g  33101  altgnsg  33104  urpropd  33185  isunit3  33194  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem3  33197  elrgspnlem4  33198  elrgspn  33199  elrgspnsubrunlem1  33200  elrgspnsubrunlem2  33201  0ringcring  33205  erlbr2d  33217  erler  33218  rlocaddval  33221  rlocmulval  33222  rloccring  33223  rloc0g  33224  rloc1r  33225  rlocf1  33226  domnprodn0  33228  rrgsubm  33236  znfermltl  33316  unitprodclb  33339  elringlsm  33343  ringlsmss  33345  lsmsnpridl  33348  cringm4  33396  ssdifidlprm  33408  mxidlprm  33420  rprmdvdspow  33483  rprmdvdsprod  33484  1arithidomlem1  33485  1arithidom  33487  1arithufdlem1  33494  1arithufdlem2  33495  1arithufdlem3  33496  1arithufdlem4  33497  dfufd2lem  33499  zringfrac  33504  ressply1evls1  33513  evl1deg1  33524  evl1deg2  33525  evl1deg3  33526  coe1vr1  33536  deg1vr  33537  gsummoncoe1fzo  33542  ply1degltdimlem  33597  ply1degltdim  33598  assarrginv  33611  evls1fldgencl  33644  rtelextdg2lem  33695  2sqr3minply  33749  cos9thpiminplylem6  33756  cos9thpiminply  33757  mdetpmtr1  33792  iistmd  33871  xrge0iifmhm  33908  xrge0pluscn  33909  pl1cn  33924  zrhcntr  33948  aks6d1c1p2  42085  aks6d1c1p3  42086  aks6d1c1p4  42087  aks6d1c1p5  42088  aks6d1c1p7  42089  aks6d1c1p6  42090  aks6d1c1p8  42091  aks6d1c1  42092  evl1gprodd  42093  aks6d1c2lem4  42103  idomnnzpownz  42108  idomnnzgmulnz  42109  ringexp0nn  42110  aks6d1c5lem0  42111  aks6d1c5lem3  42113  aks6d1c5lem2  42114  aks6d1c5  42115  deg1gprod  42116  deg1pow  42117  aks6d1c6lem1  42146  aks6d1c6lem2  42147  aks6d1c6lem3  42148  aks5lem2  42163  aks5lem3a  42165  unitscyglem5  42175  aks5lem7  42176  domnexpgn0cl  42499  abvexp  42508  fidomncyc  42511  pwsgprod  42520  evlsvvvallem  42537  evlsvvval  42539  evlsexpval  42543  selvvvval  42561  evlselv  42563  mhphf  42573  hbtlem4  43102  mon1psubm  43175  deg1mhm  43176  amgm2d  44174  amgm3d  44175  amgm4d  44176  2zrngmmgm  48240  2zrngmsgrp  48241  2zrngnring  48246  cznrng  48249  cznnring  48250  mgpsumunsn  48349  mgpsumz  48350  mgpsumn  48351  invginvrid  48355  ply1vr1smo  48371  ply1mulgsumlem4  48378  ply1mulgsum  48379  elmgpcntrd  48993  amgmlemALT  49792  amgmw2d  49793