Theorem mgpbas 20034

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

Syntax hints:   = wceq 1541  ‘cfv 6543  Basecbs 17148  ._rcmulr 17202  mulGrpcmgp 20028

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 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

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 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-plusg 17214  df-mgp 20029

This theorem is referenced by:  mgptopn  20040  mgpress  20043  mgpressOLD  20044  prdsmgp  20045  rngass  20053  rngcl  20058  isrngd  20067  rngpropd  20068  dfur2  20078  srgcl  20087  srgass  20088  srgideu  20089  srgidcl  20093  srgidmlem  20095  issrgid  20098  srg1zr  20109  srgpcomp  20112  srgpcompp  20113  srgpcomppsc  20114  srgbinomlem1  20120  srgbinomlem4  20123  srgbinomlem  20124  srgbinom  20125  csrgbinom  20126  ringcl  20144  crngcom  20145  iscrng2  20146  ringass  20147  ringideu  20148  crngbascntr  20149  ringidcl  20154  ringidmlem  20156  isringid  20159  ringidss  20165  isringrng  20175  ringpropd  20176  crngpropd  20177  isringd  20179  iscrngd  20180  ring1  20198  gsummgp0  20206  pwspjmhmmgpd  20216  pwsexpg  20217  xpsring1d  20221  oppr1  20241  unitgrpbas  20273  unitsubm  20277  rngidpropd  20306  isrnghmmul  20333  rnghmf1o  20343  idrnghm  20349  dfrhm2  20365  rhmmul  20377  isrhm2d  20378  idrhm  20381  rhmf1o  20382  pwsco1rhm  20393  pwsco2rhm  20394  c0rhm  20423  c0rnghm  20424  rhmimasubrnglem  20453  rhmimasubrng  20454  cntzsubrng  20455  subrgsubm  20475  issubrg3  20490  cntzsubr  20496  pwsdiagrhm  20497  rhmpropd  20499  isdrng2  20514  drngmcl  20517  drngid2  20521  isdrngd  20533  isdrngdOLD  20535  subrgacs  20559  cntzsdrg  20561  subdrgint  20562  primefld  20564  rlmscaf  20976  rnglidlmmgm  21034  rnglidlmsgrp  21035  rng2idl1cntr  21064  xrsmcmn  21168  cnfldexp  21178  cnmsubglem  21208  expmhm  21214  nn0srg  21215  rge0srg  21216  expghm  21246  cnmsgnbas  21350  sraassab  21641  sraassaOLD  21643  assamulgscmlem1  21672  assamulgscmlem2  21673  psrcrng  21752  mplcoe3  21812  mplcoe5lem  21813  mplcoe5  21814  mplbas2  21816  evlslem3  21862  evlslem6  21863  evlslem1  21864  evlsgsummul  21874  evlspw  21875  mpfind  21889  mhppwdeg  21912  ply1moncl  22013  coe1tm  22015  coe1pwmul  22021  ply1scltm  22023  ply1coefsupp  22039  ply1coe  22040  gsummoncoe1  22048  lply1binomsc  22051  evls1gsummul  22064  evls1pw  22065  evl1expd  22084  evl1gsummul  22099  evl1scvarpw  22102  evl1scvarpwval  22103  evl1gsummon  22104  ringvcl  22120  mamuvs2  22126  matgsumcl  22182  madetsmelbas  22186  madetsmelbas2  22187  mat1mhm  22206  scmatmhm  22256  mdetleib2  22310  mdetf  22317  m1detdiag  22319  mdetdiaglem  22320  mdetdiag  22321  mdetdiagid  22322  mdetrlin  22324  mdetrsca  22325  mdetralt  22330  mdetunilem7  22340  mdetunilem8  22341  mdetuni0  22343  m2detleiblem2  22350  m2detleiblem3  22351  m2detleiblem4  22352  smadiadetlem4  22391  mat2pmatmhm  22455  pmatcollpwscmatlem1  22511  mply1topmatcllem  22525  mply1topmatcl  22527  pm2mpghm  22538  pm2mpmhm  22542  monmat2matmon  22546  pm2mp  22547  chpscmat  22564  chpscmatgsumbin  22566  chpscmatgsummon  22567  chp0mat  22568  chpidmat  22569  chfacfscmulcl  22579  chfacfscmul0  22580  chfacfscmulgsum  22582  chfacfpmmulcl  22583  chfacfpmmul0  22584  chfacfpmmulgsum  22586  chfacfpmmulgsum2  22587  cayhamlem1  22588  cpmadugsumlemB  22596  cpmadugsumlemC  22597  cpmadugsumlemF  22598  cayhamlem2  22606  cayhamlem4  22610  nrgtrg  24427  deg1pw  25862  ply1remlem  25904  fta1blem  25910  plypf1  25950  efabl  26283  efsubm  26284  amgm  26719  wilthlem2  26797  wilthlem3  26798  dchrelbas2  26964  dchrelbas3  26965  dchrzrhmul  26973  dchrmulcl  26976  dchrn0  26977  dchrinvcl  26980  dchrfi  26982  dchrsum2  26995  sum2dchr  27001  lgsqrlem1  27073  lgsqrlem2  27074  lgsqrlem3  27075  lgsqrlem4  27076  lgseisenlem3  27104  lgseisenlem4  27105  dchrisum0flblem1  27235  cntrcrng  32472  psgnid  32514  cnmsgn0g  32563  altgnsg  32566  urpropd  32636  freshmansdream  32639  frobrhm  32640  fermltlchr  32740  znfermltl  32741  elringlsm  32765  ringlsmss  32767  lsmsnpridl  32770  cringm4  32827  mxidlprm  32848  evls1fpws  32908  ply1fermltlchr  32924  gsummoncoe1fzo  32931  ply1degltdimlem  32983  ply1degltdim  32984  evls1fldgencl  33021  mdetpmtr1  33089  iistmd  33168  xrge0iifmhm  33205  xrge0pluscn  33206  pl1cn  33221  pwsgprod  41416  evlsvvvallem  41435  evlsvvval  41437  evlsexpval  41441  selvvvval  41459  evlselv  41461  mhphf  41471  hbtlem4  42170  idomrootle  42239  isdomn3  42248  mon1psubm  42250  deg1mhm  42251  amgm2d  43252  amgm3d  43253  amgm4d  43254  2zrngmmgm  46933  2zrngmsgrp  46934  2zrngnring  46939  cznrng  46942  cznnring  46943  mgpsumunsn  47126  mgpsumz  47127  mgpsumn  47128  invginvrid  47132  ply1vr1smo  47151  ply1mulgsumlem4  47158  ply1mulgsum  47159  amgmlemALT  47938  amgmw2d  47939