Theorem mgpbas 20345

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 2761	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20343	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17370	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17438	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19544	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2784	1 ⊢ 𝐵 = (Base‘𝑀)

This proof depends on syntax axioms:   = wceq 1570  ‘cfv 6531  Basecbs 17367  ._rcmulr 17409  mulGrpcmgp 20340

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  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 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-nn 12317  df-2 12386  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-plusg 17421  df-mgp 20341

This theorem is used by:  mgptopn  20348  mgpress  20350  prdsmgp  20351  elmgplsm  20352  rngass  20361  rngcl  20366  isrngd  20375  rngpropd  20376  rng1zrlem  20383  dfur2  20390  srgcl  20399  srgass  20400  srgideu  20401  srgidcl  20405  srgidmlem  20407  issrgid  20410  srgpcomp  20424  srgpcompp  20425  srgpcomppsc  20426  srgbinomlem1  20432  srgbinomlem4  20435  srgbinomlem  20436  srgbinom  20437  csrgbinom  20438  ringcl  20457  crngcom  20458  iscrng2  20459  ringass  20460  ringideu  20461  crngbascntr  20463  ringidcl  20474  ringidmlem  20477  isringid  20480  ringidss  20486  isringrng  20496  dfring3  20498  ringpropd  20499  crngpropd  20500  isringd  20502  iscrngd  20503  ring1  20521  gsummgp0  20527  pwspjmhmmgpd  20537  pwsexpg  20538  pwsgprod  20539  xpsring1d  20543  oppr1  20560  unitgrpbas  20592  unitsubm  20596  rngidpropd  20625  isrnghmmul  20652  rnghmf1o  20662  idrnghm  20668  dfrhm2  20684  rhmmul  20700  isrhm2d  20701  idrhm  20705  rhmf1o  20707  pwsco1rhm  20721  pwsco2rhm  20722  c0rhm  20766  c0rnghm  20767  rhmimasubrnglem  20797  rhmimasubrng  20798  cntzsubrng  20799  subrgsubm  20817  issubrg3  20832  cntzsubr  20838  pwsdiagrhm  20839  rhmpropd  20841  isdomn3  20946  isdrng2  20977  isdrng3lem0  20984  isdrng3lem1  20985  drngid2  20990  isdrngd  21002  isdrngdOLD  21004  subrgacs  21037  cntzsdrg  21039  subdrgint  21040  primefld  21042  rlmscaf  21462  rnglidlmmgm  21513  rnglidlmsgrp  21514  rng2idl1cntr  21581  cringm4  21607  ssdifidlprm  21622  prmidlsubm  21623  xrsmcmn  21681  cnfldexp  21691  cnmsubglem  21716  expmhm  21722  nn0srg  21723  rge0srg  21724  expghm  21761  fermltlchr  21815  freshmansdream  21860  frobrhm  21861  cnmsgnbas  21864  sraassab  22156  assamulgscmlem1  22187  assamulgscmlem2  22188  psrcrng  22259  mplcoe3  22327  mplcoe5lem  22328  mplcoe5  22329  mplbas2  22331  evlslem3  22369  evlslem6  22370  evlslem1  22371  evlsvvvallem  22380  evlsvvval  22382  evlsgsummul  22386  evlspw  22387  mpfind  22404  evlsexpval  22417  selvvvval  22431  mhppwdeg  22451  psdpw  22471  ply1moncl  22570  coe1tm  22572  coe1pwmul  22578  ply1scltm  22580  ply1idvr1  22593  ply1coefsupp  22595  ply1coe  22596  gsummoncoe1  22606  lply1binomsc  22609  ply1fermltlchr  22610  evls1gsummul  22623  evls1pw  22624  evl1expd  22643  evl1gsummul  22658  evl1scvarpw  22661  evl1scvarpwval  22662  evl1gsummon  22663  evls1fpws  22667  rhmply1mon  22684  ringvcl  22695  mamuvs2  22701  matgsumcl  22755  madetsmelbas  22759  madetsmelbas2  22760  mat1mhm  22779  scmatmhm  22829  mdetleib2  22883  mdetf  22890  m1detdiag  22892  mdetdiaglem  22893  mdetdiag  22894  mdetdiagid  22895  mdetrlin  22897  mdetrsca  22898  mdetralt  22903  mdetunilem7  22913  mdetunilem8  22914  mdetuni0  22916  m2detleiblem2  22923  m2detleiblem3  22924  m2detleiblem4  22925  smadiadetlem4  22964  mat2pmatmhm  23031  pmatcollpwscmatlem1  23087  mply1topmatcllem  23101  mply1topmatcl  23103  pm2mpghm  23114  pm2mpmhm  23118  monmat2matmon  23122  pm2mp  23123  chpscmat  23140  chpscmatgsumbin  23142  chpscmatgsummon  23143  chp0mat  23144  chpidmat  23145  chfacfscmulcl  23155  chfacfscmul0  23156  chfacfscmulgsum  23158  chfacfpmmulcl  23159  chfacfpmmul0  23160  chfacfpmmulgsum  23162  chfacfpmmulgsum2  23163  cayhamlem1  23164  cpmadugsumlemB  23172  cpmadugsumlemC  23173  cpmadugsumlemF  23174  cayhamlem2  23182  cayhamlem4  23186  nrgtrg  24989  deg1pw  26419  ply1remlem  26463  fta1blem  26469  idomrootle  26471  plypf1  26511  efabl  26860  efsubm  26861  amgm  27300  wilthlem2  27378  wilthlem3  27379  dchrelbas2  27546  dchrelbas3  27547  dchrzrhmul  27555  dchrmulcl  27558  dchrn0  27559  dchrinvcl  27562  dchrfi  27564  dchrsum2  27577  sum2dchr  27583  lgsqrlem1  27655  lgsqrlem2  27656  lgsqrlem3  27657  lgsqrlem4  27658  lgseisenlem3  27686  lgseisenlem4  27687  dchrisum0flblem1  27817  zsoring  28777  cntrcrng  33624  psgnid  33640  cnmsgn0g  33689  altgnsg  33692  urpropd  33773  ringm1expp1  33776  isunit3  33783  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnlem3  33787  elrgspnlem4  33788  elrgspn  33789  elrgspnsubrunlem1  33790  elrgspnsubrunlem2  33791  0ringcring  33795  erlbr2d  33807  erler  33808  erld2  33809  rlocaddval  33812  rlocmulval  33813  rloccring  33814  rloc0g  33815  rloc1r  33816  rlocf1  33817  rlocinvunit  33818  rlocisunit  33819  domnprodn0  33821  domnprodeq0  33822  rrgsubm  33827  znfermltl  33904  unitprodclb  33926  ringlsmss  33930  lsmsnpridl  33933  mxidlprm  33977  rprmdvdspow  34047  rprmdvdsprod  34048  1arithidomlem1  34049  1arithidom  34051  1arithufdlem1  34058  1arithufdlem2  34059  1arithufdlem3  34060  1arithufdlem4  34061  dfufd2lem  34063  zringfrac  34068  ressply1evls1  34079  evl1deg1  34090  evl1deg2  34091  evl1deg3  34092  evls1monply1  34093  deg1prod  34097  ply1coedeg  34103  coe1vr1  34105  deg1vr  34106  gsummoncoe1fzo  34111  evlextv  34156  psrmonprod  34166  mplmonprod  34168  vietalem  34193  vieta  34194  srapwov  34203  ply1degltdimlem  34236  ply1degltdim  34237  assarrginv  34250  evls1fldgencl  34284  extdgfialglem1  34306  extdgfialglem2  34307  rtelextdg2lem  34340  2sqr3minply  34394  cos9thpiminplylem6  34401  cos9thpiminply  34402  mdetpmtr1  34437  iistmd  34516  xrge0iifmhm  34553  xrge0pluscn  34554  pl1cn  34569  zrhcntr  34593  aks6d1c1p2  43127  aks6d1c1p3  43128  aks6d1c1p4  43129  aks6d1c1p5  43130  aks6d1c1p7  43131  aks6d1c1p6  43132  aks6d1c1p8  43133  aks6d1c1  43134  evl1gprodd  43135  aks6d1c2lem4  43145  idomnnzpownz  43150  idomnnzgmulnz  43151  ringexp0nn  43152  aks6d1c5lem0  43153  aks6d1c5lem3  43155  aks6d1c5lem2  43156  aks6d1c5  43157  deg1gprod  43158  deg1pow  43159  aks6d1c6lem1  43188  aks6d1c6lem2  43189  aks6d1c6lem3  43190  aks5lem2  43205  aks5lem3a  43207  unitscyglem5  43217  aks5lem7  43218  domnexpgn0cl  43549  abvexp  43558  fidomncyc  43561  evlselv  43579  mhphf  43587  hbtlem4  44086  mon1psubm  44159  deg1mhm  44160  amgm2d  45157  amgm3d  45158  amgm4d  45159  2zrngmmgm  49293  2zrngmsgrp  49294  2zrngnring  49299  cznrng  49302  cznnring  49303  mgpsumunsn  49417  mgpsumz  49418  mgpsumn  49419  invginvrid  49423  ply1vr1smo  49439  ply1mulgsumlem4  49445  ply1mulgsum  49446  elmgpcntrd  50057  amgmlemALT  50932  amgmw2d  50933