Theorem mgpbas 20080

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 2736	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20078	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17139	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17207	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19279	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2759	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1541  ‘cfv 6492  Basecbs 17136  ._rcmulr 17178  mulGrpcmgp 20075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-2 12208  df-sets 17091  df-slot 17109  df-ndx 17121  df-base 17137  df-plusg 17190  df-mgp 20076

This theorem is referenced by:  mgptopn  20083  mgpress  20085  prdsmgp  20086  rngass  20094  rngcl  20099  isrngd  20108  rngpropd  20109  dfur2  20119  srgcl  20128  srgass  20129  srgideu  20130  srgidcl  20134  srgidmlem  20136  issrgid  20139  srg1zr  20150  srgpcomp  20153  srgpcompp  20154  srgpcomppsc  20155  srgbinomlem1  20161  srgbinomlem4  20164  srgbinomlem  20165  srgbinom  20166  csrgbinom  20167  ringcl  20185  crngcom  20186  iscrng2  20187  ringass  20188  ringideu  20189  crngbascntr  20191  ringidcl  20200  ringidmlem  20203  isringid  20206  ringidss  20212  isringrng  20222  ringpropd  20223  crngpropd  20224  isringd  20226  iscrngd  20227  ring1  20245  gsummgp0  20253  pwspjmhmmgpd  20263  pwsexpg  20264  pwsgprod  20265  xpsring1d  20269  oppr1  20286  unitgrpbas  20318  unitsubm  20322  rngidpropd  20351  isrnghmmul  20378  rnghmf1o  20388  idrnghm  20394  dfrhm2  20410  rhmmul  20421  isrhm2d  20422  idrhm  20425  rhmf1o  20426  pwsco1rhm  20435  pwsco2rhm  20436  c0rhm  20467  c0rnghm  20468  rhmimasubrnglem  20498  rhmimasubrng  20499  cntzsubrng  20500  subrgsubm  20518  issubrg3  20533  cntzsubr  20539  pwsdiagrhm  20540  rhmpropd  20542  isdomn3  20648  isdrng2  20676  drngmclOLD  20684  drngid2  20685  isdrngd  20698  isdrngdOLD  20700  subrgacs  20733  cntzsdrg  20735  subdrgint  20736  primefld  20738  rlmscaf  21159  rnglidlmmgm  21200  rnglidlmsgrp  21201  rng2idl1cntr  21260  xrsmcmn  21346  cnfldexp  21359  cnmsubglem  21385  expmhm  21391  nn0srg  21392  rge0srg  21393  expghm  21430  fermltlchr  21484  freshmansdream  21529  frobrhm  21530  cnmsgnbas  21533  sraassab  21823  sraassaOLD  21825  assamulgscmlem1  21855  assamulgscmlem2  21856  psrcrng  21927  mplcoe3  21993  mplcoe5lem  21994  mplcoe5  21995  mplbas2  21997  evlslem3  22035  evlslem6  22036  evlslem1  22037  evlsvvvallem  22046  evlsvvval  22048  evlsgsummul  22052  evlspw  22053  mpfind  22070  mhppwdeg  22093  psdpw  22113  ply1moncl  22213  coe1tm  22215  coe1pwmul  22221  ply1scltm  22223  ply1idvr1  22238  ply1coefsupp  22241  ply1coe  22242  gsummoncoe1  22252  lply1binomsc  22255  ply1fermltlchr  22256  evls1gsummul  22269  evls1pw  22270  evl1expd  22289  evl1gsummul  22304  evl1scvarpw  22307  evl1scvarpwval  22308  evl1gsummon  22309  evls1fpws  22313  rhmply1mon  22333  ringvcl  22344  mamuvs2  22350  matgsumcl  22404  madetsmelbas  22408  madetsmelbas2  22409  mat1mhm  22428  scmatmhm  22478  mdetleib2  22532  mdetf  22539  m1detdiag  22541  mdetdiaglem  22542  mdetdiag  22543  mdetdiagid  22544  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  mdetunilem7  22562  mdetunilem8  22563  mdetuni0  22565  m2detleiblem2  22572  m2detleiblem3  22573  m2detleiblem4  22574  smadiadetlem4  22613  mat2pmatmhm  22677  pmatcollpwscmatlem1  22733  mply1topmatcllem  22747  mply1topmatcl  22749  pm2mpghm  22760  pm2mpmhm  22764  monmat2matmon  22768  pm2mp  22769  chpscmat  22786  chpscmatgsumbin  22788  chpscmatgsummon  22789  chp0mat  22790  chpidmat  22791  chfacfscmulcl  22801  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmulcl  22805  chfacfpmmul0  22806  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cayhamlem2  22828  cayhamlem4  22832  nrgtrg  24634  deg1pw  26082  ply1remlem  26126  fta1blem  26132  idomrootle  26134  plypf1  26173  efabl  26515  efsubm  26516  amgm  26957  wilthlem2  27035  wilthlem3  27036  dchrelbas2  27204  dchrelbas3  27205  dchrzrhmul  27213  dchrmulcl  27216  dchrn0  27217  dchrinvcl  27220  dchrfi  27222  dchrsum2  27235  sum2dchr  27241  lgsqrlem1  27313  lgsqrlem2  27314  lgsqrlem3  27315  lgsqrlem4  27316  lgseisenlem3  27344  lgseisenlem4  27345  dchrisum0flblem1  27475  zsoring  28405  cntrcrng  33163  psgnid  33179  cnmsgn0g  33228  altgnsg  33231  urpropd  33313  ringm1expp1  33316  isunit3  33323  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspn  33328  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  0ringcring  33334  erlbr2d  33346  erler  33347  rlocaddval  33350  rlocmulval  33351  rloccring  33352  rloc0g  33353  rloc1r  33354  rlocf1  33355  domnprodn0  33357  domnprodeq0  33358  rrgsubm  33366  znfermltl  33447  unitprodclb  33470  elringlsm  33474  ringlsmss  33476  lsmsnpridl  33479  cringm4  33527  ssdifidlprm  33539  mxidlprm  33551  rprmdvdspow  33614  rprmdvdsprod  33615  1arithidomlem1  33616  1arithidom  33618  1arithufdlem1  33625  1arithufdlem2  33626  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  zringfrac  33635  ressply1evls1  33646  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  evls1monply1  33660  deg1prod  33664  ply1coedeg  33670  coe1vr1  33672  deg1vr  33673  gsummoncoe1fzo  33678  evlextv  33707  vietalem  33735  vieta  33736  srapwov  33745  ply1degltdimlem  33779  ply1degltdim  33780  assarrginv  33793  evls1fldgencl  33827  extdgfialglem1  33849  extdgfialglem2  33850  rtelextdg2lem  33883  2sqr3minply  33937  cos9thpiminplylem6  33944  cos9thpiminply  33945  mdetpmtr1  33980  iistmd  34059  xrge0iifmhm  34096  xrge0pluscn  34097  pl1cn  34112  zrhcntr  34136  aks6d1c1p2  42363  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1p7  42367  aks6d1c1p6  42368  aks6d1c1p8  42369  aks6d1c1  42370  evl1gprodd  42371  aks6d1c2lem4  42381  idomnnzpownz  42386  idomnnzgmulnz  42387  ringexp0nn  42388  aks6d1c5lem0  42389  aks6d1c5lem3  42391  aks6d1c5lem2  42392  aks6d1c5  42393  deg1gprod  42394  deg1pow  42395  aks6d1c6lem1  42424  aks6d1c6lem2  42425  aks6d1c6lem3  42426  aks5lem2  42441  aks5lem3a  42443  unitscyglem5  42453  aks5lem7  42454  domnexpgn0cl  42778  abvexp  42787  fidomncyc  42790  evlsexpval  42813  selvvvval  42828  evlselv  42830  mhphf  42840  hbtlem4  43368  mon1psubm  43441  deg1mhm  43442  amgm2d  44439  amgm3d  44440  amgm4d  44441  2zrngmmgm  48498  2zrngmsgrp  48499  2zrngnring  48504  cznrng  48507  cznnring  48508  mgpsumunsn  48607  mgpsumz  48608  mgpsumn  48609  invginvrid  48613  ply1vr1smo  48629  ply1mulgsumlem4  48635  ply1mulgsum  48636  elmgpcntrd  49250  amgmlemALT  50048  amgmw2d  50049