Theorem mgpbas 20157

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 2734	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20154	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17247	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17327	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19380	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2762	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1536  ‘cfv 6562  Basecbs 17244  ._rcmulr 17298  mulGrpcmgp 20151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-plusg 17310  df-mgp 20152

This theorem is referenced by:  mgptopn  20163  mgpress  20166  mgpressOLD  20167  prdsmgp  20168  rngass  20176  rngcl  20181  isrngd  20190  rngpropd  20191  dfur2  20201  srgcl  20210  srgass  20211  srgideu  20212  srgidcl  20216  srgidmlem  20218  issrgid  20221  srg1zr  20232  srgpcomp  20235  srgpcompp  20236  srgpcomppsc  20237  srgbinomlem1  20243  srgbinomlem4  20246  srgbinomlem  20247  srgbinom  20248  csrgbinom  20249  ringcl  20267  crngcom  20268  iscrng2  20269  ringass  20270  ringideu  20271  crngbascntr  20273  ringidcl  20279  ringidmlem  20281  isringid  20284  ringidss  20290  isringrng  20300  ringpropd  20301  crngpropd  20302  isringd  20304  iscrngd  20305  ring1  20323  gsummgp0  20331  pwspjmhmmgpd  20341  pwsexpg  20342  xpsring1d  20346  oppr1  20366  unitgrpbas  20398  unitsubm  20402  rngidpropd  20431  isrnghmmul  20458  rnghmf1o  20468  idrnghm  20474  dfrhm2  20490  rhmmul  20502  isrhm2d  20503  idrhm  20506  rhmf1o  20507  pwsco1rhm  20518  pwsco2rhm  20519  c0rhm  20550  c0rnghm  20551  rhmimasubrnglem  20581  rhmimasubrng  20582  cntzsubrng  20583  subrgsubm  20601  issubrg3  20616  cntzsubr  20622  pwsdiagrhm  20623  rhmpropd  20625  isdomn3  20731  isdrng2  20759  drngmclOLD  20767  drngid2  20768  isdrngd  20781  isdrngdOLD  20783  subrgacs  20817  cntzsdrg  20819  subdrgint  20820  primefld  20822  rlmscaf  21231  rnglidlmmgm  21272  rnglidlmsgrp  21273  rng2idl1cntr  21332  xrsmcmn  21421  cnfldexp  21434  cnmsubglem  21465  expmhm  21471  nn0srg  21472  rge0srg  21473  expghm  21503  fermltlchr  21561  freshmansdream  21610  frobrhm  21611  cnmsgnbas  21613  sraassab  21905  sraassaOLD  21907  assamulgscmlem1  21936  assamulgscmlem2  21937  psrcrng  22009  mplcoe3  22073  mplcoe5lem  22074  mplcoe5  22075  mplbas2  22077  evlslem3  22121  evlslem6  22122  evlslem1  22123  evlsgsummul  22133  evlspw  22134  mpfind  22148  mhppwdeg  22171  ply1moncl  22289  coe1tm  22291  coe1pwmul  22297  ply1scltm  22299  ply1idvr1  22313  ply1coefsupp  22316  ply1coe  22317  gsummoncoe1  22327  lply1binomsc  22330  ply1fermltlchr  22331  evls1gsummul  22344  evls1pw  22345  evl1expd  22364  evl1gsummul  22379  evl1scvarpw  22382  evl1scvarpwval  22383  evl1gsummon  22384  evls1fpws  22388  rhmply1mon  22408  ringvcl  22419  mamuvs2  22425  matgsumcl  22481  madetsmelbas  22485  madetsmelbas2  22486  mat1mhm  22505  scmatmhm  22555  mdetleib2  22609  mdetf  22616  m1detdiag  22618  mdetdiaglem  22619  mdetdiag  22620  mdetdiagid  22621  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  mdetunilem7  22639  mdetunilem8  22640  mdetuni0  22642  m2detleiblem2  22649  m2detleiblem3  22650  m2detleiblem4  22651  smadiadetlem4  22690  mat2pmatmhm  22754  pmatcollpwscmatlem1  22810  mply1topmatcllem  22824  mply1topmatcl  22826  pm2mpghm  22837  pm2mpmhm  22841  monmat2matmon  22845  pm2mp  22846  chpscmat  22863  chpscmatgsumbin  22865  chpscmatgsummon  22866  chp0mat  22867  chpidmat  22868  chfacfscmulcl  22878  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmulcl  22882  chfacfpmmul0  22883  chfacfpmmulgsum  22885  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  cayhamlem2  22905  cayhamlem4  22909  nrgtrg  24726  deg1pw  26174  ply1remlem  26218  fta1blem  26224  idomrootle  26226  plypf1  26265  efabl  26606  efsubm  26607  amgm  27048  wilthlem2  27126  wilthlem3  27127  dchrelbas2  27295  dchrelbas3  27296  dchrzrhmul  27304  dchrmulcl  27307  dchrn0  27308  dchrinvcl  27311  dchrfi  27313  dchrsum2  27326  sum2dchr  27332  lgsqrlem1  27404  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  lgseisenlem3  27435  lgseisenlem4  27436  dchrisum0flblem1  27566  cntrcrng  33055  psgnid  33099  cnmsgn0g  33148  altgnsg  33151  urpropd  33221  isunit3  33230  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  0ringcring  33238  erlbr2d  33250  erler  33251  rlocaddval  33254  rlocmulval  33255  rloccring  33256  rloc0g  33257  rloc1r  33258  rlocf1  33259  domnprodn0  33261  rrgsubm  33267  znfermltl  33373  unitprodclb  33396  elringlsm  33400  ringlsmss  33402  lsmsnpridl  33405  cringm4  33453  ssdifidlprm  33465  mxidlprm  33477  rprmdvdspow  33540  rprmdvdsprod  33541  1arithidomlem1  33542  1arithidom  33544  1arithufdlem1  33551  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  dfufd2lem  33556  zringfrac  33561  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  coe1vr1  33592  deg1vr  33593  gsummoncoe1fzo  33597  ply1degltdimlem  33649  ply1degltdim  33650  assarrginv  33663  evls1fldgencl  33694  rtelextdg2lem  33731  2sqr3minply  33752  mdetpmtr1  33783  iistmd  33862  xrge0iifmhm  33899  xrge0pluscn  33900  pl1cn  33915  zrhcntr  33941  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c1p5  42093  aks6d1c1p7  42094  aks6d1c1p6  42095  aks6d1c1p8  42096  aks6d1c1  42097  evl1gprodd  42098  aks6d1c2lem4  42108  idomnnzpownz  42113  idomnnzgmulnz  42114  ringexp0nn  42115  aks6d1c5lem0  42116  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c5  42120  deg1gprod  42121  deg1pow  42122  aks6d1c6lem1  42151  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks5lem2  42168  aks5lem3a  42170  unitscyglem5  42180  aks5lem7  42181  domnexpgn0cl  42509  abvexp  42518  fidomncyc  42521  pwsgprod  42530  evlsvvvallem  42547  evlsvvval  42549  evlsexpval  42553  selvvvval  42571  evlselv  42573  mhphf  42583  hbtlem4  43114  mon1psubm  43187  deg1mhm  43188  amgm2d  44187  amgm3d  44188  amgm4d  44189  2zrngmmgm  48095  2zrngmsgrp  48096  2zrngnring  48101  cznrng  48104  cznnring  48105  mgpsumunsn  48205  mgpsumz  48206  mgpsumn  48207  invginvrid  48211  ply1vr1smo  48227  ply1mulgsumlem4  48234  ply1mulgsum  48235  elmgpcntrd  48793  amgmlemALT  49033  amgmw2d  49034