Theorem mgpbas 20103

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 2735	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20101	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17229	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17299	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19331	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2758	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1540  ‘cfv 6530  Basecbs 17226  ._rcmulr 17270  mulGrpcmgp 20098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-2 12301  df-sets 17181  df-slot 17199  df-ndx 17211  df-base 17227  df-plusg 17282  df-mgp 20099

This theorem is referenced by:  mgptopn  20106  mgpress  20108  prdsmgp  20109  rngass  20117  rngcl  20122  isrngd  20131  rngpropd  20132  dfur2  20142  srgcl  20151  srgass  20152  srgideu  20153  srgidcl  20157  srgidmlem  20159  issrgid  20162  srg1zr  20173  srgpcomp  20176  srgpcompp  20177  srgpcomppsc  20178  srgbinomlem1  20184  srgbinomlem4  20187  srgbinomlem  20188  srgbinom  20189  csrgbinom  20190  ringcl  20208  crngcom  20209  iscrng2  20210  ringass  20211  ringideu  20212  crngbascntr  20214  ringidcl  20223  ringidmlem  20226  isringid  20229  ringidss  20235  isringrng  20245  ringpropd  20246  crngpropd  20247  isringd  20249  iscrngd  20250  ring1  20268  gsummgp0  20276  pwspjmhmmgpd  20286  pwsexpg  20287  xpsring1d  20291  oppr1  20308  unitgrpbas  20340  unitsubm  20344  rngidpropd  20373  isrnghmmul  20400  rnghmf1o  20410  idrnghm  20416  dfrhm2  20432  rhmmul  20444  isrhm2d  20445  idrhm  20448  rhmf1o  20449  pwsco1rhm  20460  pwsco2rhm  20461  c0rhm  20492  c0rnghm  20493  rhmimasubrnglem  20523  rhmimasubrng  20524  cntzsubrng  20525  subrgsubm  20543  issubrg3  20558  cntzsubr  20564  pwsdiagrhm  20565  rhmpropd  20567  isdomn3  20673  isdrng2  20701  drngmclOLD  20709  drngid2  20710  isdrngd  20723  isdrngdOLD  20725  subrgacs  20758  cntzsdrg  20760  subdrgint  20761  primefld  20763  rlmscaf  21163  rnglidlmmgm  21204  rnglidlmsgrp  21205  rng2idl1cntr  21264  xrsmcmn  21352  cnfldexp  21365  cnmsubglem  21396  expmhm  21402  nn0srg  21403  rge0srg  21404  expghm  21434  fermltlchr  21488  freshmansdream  21533  frobrhm  21534  cnmsgnbas  21536  sraassab  21826  sraassaOLD  21828  assamulgscmlem1  21857  assamulgscmlem2  21858  psrcrng  21930  mplcoe3  21994  mplcoe5lem  21995  mplcoe5  21996  mplbas2  21998  evlslem3  22036  evlslem6  22037  evlslem1  22038  evlsgsummul  22048  evlspw  22049  mpfind  22063  mhppwdeg  22086  psdpw  22106  ply1moncl  22206  coe1tm  22208  coe1pwmul  22214  ply1scltm  22216  ply1idvr1  22230  ply1coefsupp  22233  ply1coe  22234  gsummoncoe1  22244  lply1binomsc  22247  ply1fermltlchr  22248  evls1gsummul  22261  evls1pw  22262  evl1expd  22281  evl1gsummul  22296  evl1scvarpw  22299  evl1scvarpwval  22300  evl1gsummon  22301  evls1fpws  22305  rhmply1mon  22325  ringvcl  22336  mamuvs2  22342  matgsumcl  22396  madetsmelbas  22400  madetsmelbas2  22401  mat1mhm  22420  scmatmhm  22470  mdetleib2  22524  mdetf  22531  m1detdiag  22533  mdetdiaglem  22534  mdetdiag  22535  mdetdiagid  22536  mdetrlin  22538  mdetrsca  22539  mdetralt  22544  mdetunilem7  22554  mdetunilem8  22555  mdetuni0  22557  m2detleiblem2  22564  m2detleiblem3  22565  m2detleiblem4  22566  smadiadetlem4  22605  mat2pmatmhm  22669  pmatcollpwscmatlem1  22725  mply1topmatcllem  22739  mply1topmatcl  22741  pm2mpghm  22752  pm2mpmhm  22756  monmat2matmon  22760  pm2mp  22761  chpscmat  22778  chpscmatgsumbin  22780  chpscmatgsummon  22781  chp0mat  22782  chpidmat  22783  chfacfscmulcl  22793  chfacfscmul0  22794  chfacfscmulgsum  22796  chfacfpmmulcl  22797  chfacfpmmul0  22798  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  cayhamlem2  22820  cayhamlem4  22824  nrgtrg  24627  deg1pw  26076  ply1remlem  26120  fta1blem  26126  idomrootle  26128  plypf1  26167  efabl  26509  efsubm  26510  amgm  26951  wilthlem2  27029  wilthlem3  27030  dchrelbas2  27198  dchrelbas3  27199  dchrzrhmul  27207  dchrmulcl  27210  dchrn0  27211  dchrinvcl  27214  dchrfi  27216  dchrsum2  27229  sum2dchr  27235  lgsqrlem1  27307  lgsqrlem2  27308  lgsqrlem3  27309  lgsqrlem4  27310  lgseisenlem3  27338  lgseisenlem4  27339  dchrisum0flblem1  27469  cntrcrng  33010  psgnid  33054  cnmsgn0g  33103  altgnsg  33106  urpropd  33173  isunit3  33182  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspn  33187  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  0ringcring  33193  erlbr2d  33205  erler  33206  rlocaddval  33209  rlocmulval  33210  rloccring  33211  rloc0g  33212  rloc1r  33213  rlocf1  33214  domnprodn0  33216  rrgsubm  33224  znfermltl  33327  unitprodclb  33350  elringlsm  33354  ringlsmss  33356  lsmsnpridl  33359  cringm4  33407  ssdifidlprm  33419  mxidlprm  33431  rprmdvdspow  33494  rprmdvdsprod  33495  1arithidomlem1  33496  1arithidom  33498  1arithufdlem1  33505  1arithufdlem2  33506  1arithufdlem3  33507  1arithufdlem4  33508  dfufd2lem  33510  zringfrac  33515  ressply1evls1  33524  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  coe1vr1  33547  deg1vr  33548  gsummoncoe1fzo  33553  ply1degltdimlem  33608  ply1degltdim  33609  assarrginv  33622  evls1fldgencl  33657  rtelextdg2lem  33706  2sqr3minply  33760  cos9thpiminplylem6  33767  cos9thpiminply  33768  mdetpmtr1  33800  iistmd  33879  xrge0iifmhm  33916  xrge0pluscn  33917  pl1cn  33932  zrhcntr  33956  aks6d1c1p2  42068  aks6d1c1p3  42069  aks6d1c1p4  42070  aks6d1c1p5  42071  aks6d1c1p7  42072  aks6d1c1p6  42073  aks6d1c1p8  42074  aks6d1c1  42075  evl1gprodd  42076  aks6d1c2lem4  42086  idomnnzpownz  42091  idomnnzgmulnz  42092  ringexp0nn  42093  aks6d1c5lem0  42094  aks6d1c5lem3  42096  aks6d1c5lem2  42097  aks6d1c5  42098  deg1gprod  42099  deg1pow  42100  aks6d1c6lem1  42129  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks5lem2  42146  aks5lem3a  42148  unitscyglem5  42158  aks5lem7  42159  domnexpgn0cl  42493  abvexp  42502  fidomncyc  42505  pwsgprod  42514  evlsvvvallem  42531  evlsvvval  42533  evlsexpval  42537  selvvvval  42555  evlselv  42557  mhphf  42567  hbtlem4  43097  mon1psubm  43170  deg1mhm  43171  amgm2d  44169  amgm3d  44170  amgm4d  44171  2zrngmmgm  48175  2zrngmsgrp  48176  2zrngnring  48181  cznrng  48184  cznnring  48185  mgpsumunsn  48284  mgpsumz  48285  mgpsumn  48286  invginvrid  48290  ply1vr1smo  48306  ply1mulgsumlem4  48313  ply1mulgsum  48314  elmgpcntrd  48927  amgmlemALT  49615  amgmw2d  49616