Theorem mgpbas 19641

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 2738	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 19638	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 16843	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 16918	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 18869	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2766	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1539  ‘cfv 6418  Basecbs 16840  ._rcmulr 16889  mulGrpcmgp 19635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-2 11966  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-plusg 16901  df-mgp 19636

This theorem is referenced by:  mgptopn  19647  mgpress  19650  mgpressOLD  19651  dfur2  19655  srgcl  19663  srgass  19664  srgideu  19665  srgidcl  19669  srgidmlem  19671  issrgid  19674  srg1zr  19680  srgpcomp  19683  srgpcompp  19684  srgpcomppsc  19685  srgbinomlem1  19691  srgbinomlem4  19694  srgbinomlem  19695  srgbinom  19696  csrgbinom  19697  ringcl  19715  crngcom  19716  iscrng2  19717  ringass  19718  ringideu  19719  ringidcl  19722  ringidmlem  19724  isringid  19727  ringidss  19731  ringpropd  19736  crngpropd  19737  isringd  19739  iscrngd  19740  ring1  19756  gsummgp0  19762  prdsmgp  19764  oppr1  19791  unitgrpbas  19823  unitsubm  19827  rngidpropd  19852  dfrhm2  19876  rhmmul  19886  isrhm2d  19887  idrhm  19890  rhmf1o  19891  pwsco1rhm  19897  pwsco2rhm  19898  isdrng2  19916  drngmcl  19919  drngid2  19922  isdrngd  19931  subrgsubm  19952  issubrg3  19967  cntzsubr  19972  pwsdiagrhm  19973  rhmpropd  19975  subrgacs  19983  cntzsdrg  19985  subdrgint  19986  primefld  19988  rlmscaf  20392  xrsmcmn  20533  cnfldexp  20543  cnmsubglem  20573  expmhm  20579  nn0srg  20580  rge0srg  20581  expghm  20609  cnmsgnbas  20695  sraassa  20984  assamulgscmlem1  21013  assamulgscmlem2  21014  psrcrng  21092  mplcoe3  21149  mplcoe5lem  21150  mplcoe5  21151  mplbas2  21153  evlslem3  21200  evlslem6  21201  evlslem1  21202  evlsgsummul  21212  evlspw  21213  mpfind  21227  mhppwdeg  21250  ply1moncl  21352  coe1tm  21354  coe1pwmul  21360  ply1scltm  21362  ply1coefsupp  21376  ply1coe  21377  gsummoncoe1  21385  lply1binomsc  21388  evls1gsummul  21401  evls1pw  21402  evl1expd  21421  evl1gsummul  21436  evl1scvarpw  21439  evl1scvarpwval  21440  evl1gsummon  21441  ringvcl  21457  mamuvs2  21463  matgsumcl  21517  madetsmelbas  21521  madetsmelbas2  21522  mat1mhm  21541  scmatmhm  21591  mdetleib2  21645  mdetf  21652  m1detdiag  21654  mdetdiaglem  21655  mdetdiag  21656  mdetdiagid  21657  mdetrlin  21659  mdetrsca  21660  mdetralt  21665  mdetunilem7  21675  mdetunilem8  21676  mdetuni0  21678  m2detleiblem2  21685  m2detleiblem3  21686  m2detleiblem4  21687  smadiadetlem4  21726  mat2pmatmhm  21790  pmatcollpwscmatlem1  21846  mply1topmatcllem  21860  mply1topmatcl  21862  pm2mpghm  21873  pm2mpmhm  21877  monmat2matmon  21881  pm2mp  21882  chpscmat  21899  chpscmatgsumbin  21901  chpscmatgsummon  21902  chp0mat  21903  chpidmat  21904  chfacfscmulcl  21914  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmulcl  21918  chfacfpmmul0  21919  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  cayhamlem2  21941  cayhamlem4  21945  nrgtrg  23760  deg1pw  25190  ply1remlem  25232  fta1blem  25238  plypf1  25278  efabl  25611  efsubm  25612  amgm  26045  wilthlem2  26123  wilthlem3  26124  dchrelbas2  26290  dchrelbas3  26291  dchrzrhmul  26299  dchrmulcl  26302  dchrn0  26303  dchrinvcl  26306  dchrfi  26308  dchrsum2  26321  sum2dchr  26327  lgsqrlem1  26399  lgsqrlem2  26400  lgsqrlem3  26401  lgsqrlem4  26402  lgseisenlem3  26430  lgseisenlem4  26431  dchrisum0flblem1  26561  cntrcrng  31224  psgnid  31266  cnmsgn0g  31315  altgnsg  31318  freshmansdream  31386  frobrhm  31387  znfermltl  31464  elringlsm  31483  ringlsmss  31485  lsmsnpridl  31488  cringm4  31524  mxidlprm  31542  ply1fermltl  31572  mdetpmtr1  31675  iistmd  31754  xrge0iifmhm  31791  xrge0pluscn  31792  pl1cn  31807  pwspjmhmmgpd  40192  pwsexpg  40193  pwsgprod  40194  evlsbagval  40198  evlsexpval  40199  mhphf  40208  hbtlem4  40867  idomrootle  40936  isdomn3  40945  mon1psubm  40947  deg1mhm  40948  amgm2d  41698  amgm3d  41699  amgm4d  41700  isringrng  45327  rngcl  45329  isrnghmmul  45339  rnghmf1o  45349  idrnghm  45354  c0rhm  45358  c0rnghm  45359  lidlmmgm  45371  lidlmsgrp  45372  2zrngmmgm  45392  2zrngmsgrp  45393  2zrngnring  45398  cznrng  45401  cznnring  45402  mgpsumunsn  45585  mgpsumz  45586  mgpsumn  45587  invginvrid  45591  ply1vr1smo  45610  ply1mulgsumlem4  45618  ply1mulgsum  45619  amgmlemALT  46393  amgmw2d  46394