Theorem mgpbas 20209

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 2765	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20207	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17260	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17328	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19408	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2788	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1563  ‘cfv 6525  Basecbs 17257  ._rcmulr 17299  mulGrpcmgp 20204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-nn 12222  df-2 12291  df-sets 17212  df-slot 17230  df-ndx 17242  df-base 17258  df-plusg 17311  df-mgp 20205

This theorem is referenced by:  mgptopn  20212  mgpress  20214  prdsmgp  20215  elmgplsm  20216  rngass  20225  rngcl  20230  isrngd  20239  rngpropd  20240  rng1zrlem  20247  dfur2  20254  srgcl  20263  srgass  20264  srgideu  20265  srgidcl  20269  srgidmlem  20271  issrgid  20274  srgpcomp  20288  srgpcompp  20289  srgpcomppsc  20290  srgbinomlem1  20296  srgbinomlem4  20299  srgbinomlem  20300  srgbinom  20301  csrgbinom  20302  ringcl  20320  crngcom  20321  iscrng2  20322  ringass  20323  ringideu  20324  crngbascntr  20326  ringidcl  20336  ringidmlem  20339  isringid  20342  ringidss  20348  isringrng  20358  ringpropd  20359  crngpropd  20360  isringd  20362  iscrngd  20363  ring1  20381  gsummgp0  20387  pwspjmhmmgpd  20397  pwsexpg  20398  pwsgprod  20399  xpsring1d  20403  oppr1  20420  unitgrpbas  20452  unitsubm  20456  rngidpropd  20485  isrnghmmul  20512  rnghmf1o  20522  idrnghm  20528  dfrhm2  20544  rhmmul  20556  isrhm2d  20557  idrhm  20560  rhmf1o  20561  pwsco1rhm  20572  pwsco2rhm  20573  c0rhm  20607  c0rnghm  20608  rhmimasubrnglem  20638  rhmimasubrng  20639  cntzsubrng  20640  subrgsubm  20658  issubrg3  20673  cntzsubr  20679  pwsdiagrhm  20680  rhmpropd  20682  isdomn3  20787  isdrng2  20815  drngid2  20823  isdrngd  20835  isdrngdOLD  20837  subrgacs  20869  cntzsdrg  20871  subdrgint  20872  primefld  20874  rlmscaf  21294  rnglidlmmgm  21341  rnglidlmsgrp  21342  rng2idl1cntr  21404  cringm4  21430  ssdifidlprm  21443  prmidlsubm  21444  xrsmcmn  21502  cnfldexp  21512  cnmsubglem  21537  expmhm  21543  nn0srg  21544  rge0srg  21545  expghm  21582  fermltlchr  21636  freshmansdream  21681  frobrhm  21682  cnmsgnbas  21685  sraassab  21975  assamulgscmlem1  22006  assamulgscmlem2  22007  psrcrng  22078  mplcoe3  22146  mplcoe5lem  22147  mplcoe5  22148  mplbas2  22150  evlslem3  22188  evlslem6  22189  evlslem1  22190  evlsvvvallem  22199  evlsvvval  22201  evlsgsummul  22205  evlspw  22206  mpfind  22223  evlsexpval  22236  selvvvval  22250  mhppwdeg  22270  psdpw  22290  ply1moncl  22389  coe1tm  22391  coe1pwmul  22397  ply1scltm  22399  ply1idvr1  22412  ply1coefsupp  22414  ply1coe  22415  gsummoncoe1  22425  lply1binomsc  22428  ply1fermltlchr  22429  evls1gsummul  22442  evls1pw  22443  evl1expd  22462  evl1gsummul  22477  evl1scvarpw  22480  evl1scvarpwval  22481  evl1gsummon  22482  evls1fpws  22486  rhmply1mon  22503  ringvcl  22514  mamuvs2  22520  matgsumcl  22574  madetsmelbas  22578  madetsmelbas2  22579  mat1mhm  22598  scmatmhm  22648  mdetleib2  22702  mdetf  22709  m1detdiag  22711  mdetdiaglem  22712  mdetdiag  22713  mdetdiagid  22714  mdetrlin  22716  mdetrsca  22717  mdetralt  22722  mdetunilem7  22732  mdetunilem8  22733  mdetuni0  22735  m2detleiblem2  22742  m2detleiblem3  22743  m2detleiblem4  22744  smadiadetlem4  22783  mat2pmatmhm  22847  pmatcollpwscmatlem1  22903  mply1topmatcllem  22917  mply1topmatcl  22919  pm2mpghm  22930  pm2mpmhm  22934  monmat2matmon  22938  pm2mp  22939  chpscmat  22956  chpscmatgsumbin  22958  chpscmatgsummon  22959  chp0mat  22960  chpidmat  22961  chfacfscmulcl  22971  chfacfscmul0  22972  chfacfscmulgsum  22974  chfacfpmmulcl  22975  chfacfpmmul0  22976  chfacfpmmulgsum  22978  chfacfpmmulgsum2  22979  cayhamlem1  22980  cpmadugsumlemB  22988  cpmadugsumlemC  22989  cpmadugsumlemF  22990  cayhamlem2  22998  cayhamlem4  23002  nrgtrg  24804  deg1pw  26235  ply1remlem  26279  fta1blem  26285  idomrootle  26287  plypf1  26326  efabl  26669  efsubm  26670  amgm  27109  wilthlem2  27187  wilthlem3  27188  dchrelbas2  27355  dchrelbas3  27356  dchrzrhmul  27364  dchrmulcl  27367  dchrn0  27368  dchrinvcl  27371  dchrfi  27373  dchrsum2  27386  sum2dchr  27392  lgsqrlem1  27464  lgsqrlem2  27465  lgsqrlem3  27466  lgsqrlem4  27467  lgseisenlem3  27495  lgseisenlem4  27496  dchrisum0flblem1  27626  zsoring  28556  cntrcrng  33309  psgnid  33325  cnmsgn0g  33374  altgnsg  33377  urpropd  33458  ringm1expp1  33461  isunit3  33468  elrgspnlem1  33470  elrgspnlem2  33471  elrgspnlem3  33472  elrgspnlem4  33473  elrgspn  33474  elrgspnsubrunlem1  33475  elrgspnsubrunlem2  33476  0ringcring  33480  erlbr2d  33492  erler  33493  erld2  33494  rlocaddval  33497  rlocmulval  33498  rloccring  33499  rloc0g  33500  rloc1r  33501  rlocf1  33502  rlocinvunit  33503  rlocisunit  33504  domnprodn0  33506  domnprodeq0  33507  rrgsubm  33512  znfermltl  33591  unitprodclb  33613  ringlsmss  33617  lsmsnpridl  33620  mxidlprm  33665  rprmdvdspow  33735  rprmdvdsprod  33736  1arithidomlem1  33737  1arithidom  33739  1arithufdlem1  33746  1arithufdlem2  33747  1arithufdlem3  33748  1arithufdlem4  33749  dfufd2lem  33751  zringfrac  33756  ressply1evls1  33767  evl1deg1  33778  evl1deg2  33779  evl1deg3  33780  evls1monply1  33781  deg1prod  33785  ply1coedeg  33791  coe1vr1  33793  deg1vr  33794  gsummoncoe1fzo  33799  evlextv  33844  psrmonprod  33854  mplmonprod  33856  vietalem  33881  vieta  33882  srapwov  33891  ply1degltdimlem  33924  ply1degltdim  33925  assarrginv  33938  evls1fldgencl  33972  extdgfialglem1  33994  extdgfialglem2  33995  rtelextdg2lem  34028  2sqr3minply  34082  cos9thpiminplylem6  34089  cos9thpiminply  34090  mdetpmtr1  34125  iistmd  34204  xrge0iifmhm  34241  xrge0pluscn  34242  pl1cn  34257  zrhcntr  34281  aks6d1c1p2  42733  aks6d1c1p3  42734  aks6d1c1p4  42735  aks6d1c1p5  42736  aks6d1c1p7  42737  aks6d1c1p6  42738  aks6d1c1p8  42739  aks6d1c1  42740  evl1gprodd  42741  aks6d1c2lem4  42751  idomnnzpownz  42756  idomnnzgmulnz  42757  ringexp0nn  42758  aks6d1c5lem0  42759  aks6d1c5lem3  42761  aks6d1c5lem2  42762  aks6d1c5  42763  deg1gprod  42764  deg1pow  42765  aks6d1c6lem1  42794  aks6d1c6lem2  42795  aks6d1c6lem3  42796  aks5lem2  42811  aks5lem3a  42813  unitscyglem5  42823  aks5lem7  42824  domnexpgn0cl  43148  abvexp  43157  fidomncyc  43160  evlselv  43178  mhphf  43186  hbtlem4  43710  mon1psubm  43783  deg1mhm  43784  amgm2d  44781  amgm3d  44782  amgm4d  44783  2zrngmmgm  48873  2zrngmsgrp  48874  2zrngnring  48879  cznrng  48882  cznnring  48883  mgpsumunsn  48993  mgpsumz  48994  mgpsumn  48995  invginvrid  48999  ply1vr1smo  49015  ply1mulgsumlem4  49021  ply1mulgsum  49022  elmgpcntrd  49635  amgmlemALT  50433  amgmw2d  50434