Theorem mgpbas 20117

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 2737	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20115	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17173	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17241	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19316	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2760	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1542  ‘cfv 6492  Basecbs 17170  ._rcmulr 17212  mulGrpcmgp 20112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  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 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-plusg 17224  df-mgp 20113

This theorem is referenced by:  mgptopn  20120  mgpress  20122  prdsmgp  20123  rngass  20131  rngcl  20136  isrngd  20145  rngpropd  20146  dfur2  20156  srgcl  20165  srgass  20166  srgideu  20167  srgidcl  20171  srgidmlem  20173  issrgid  20176  srg1zr  20187  srgpcomp  20190  srgpcompp  20191  srgpcomppsc  20192  srgbinomlem1  20198  srgbinomlem4  20201  srgbinomlem  20202  srgbinom  20203  csrgbinom  20204  ringcl  20222  crngcom  20223  iscrng2  20224  ringass  20225  ringideu  20226  crngbascntr  20228  ringidcl  20237  ringidmlem  20240  isringid  20243  ringidss  20249  isringrng  20259  ringpropd  20260  crngpropd  20261  isringd  20263  iscrngd  20264  ring1  20282  gsummgp0  20288  pwspjmhmmgpd  20298  pwsexpg  20299  pwsgprod  20300  xpsring1d  20304  oppr1  20321  unitgrpbas  20353  unitsubm  20357  rngidpropd  20386  isrnghmmul  20413  rnghmf1o  20423  idrnghm  20429  dfrhm2  20445  rhmmul  20456  isrhm2d  20457  idrhm  20460  rhmf1o  20461  pwsco1rhm  20470  pwsco2rhm  20471  c0rhm  20502  c0rnghm  20503  rhmimasubrnglem  20533  rhmimasubrng  20534  cntzsubrng  20535  subrgsubm  20553  issubrg3  20568  cntzsubr  20574  pwsdiagrhm  20575  rhmpropd  20577  isdomn3  20683  isdrng2  20711  drngmclOLD  20719  drngid2  20720  isdrngd  20733  isdrngdOLD  20735  subrgacs  20768  cntzsdrg  20770  subdrgint  20771  primefld  20773  rlmscaf  21194  rnglidlmmgm  21235  rnglidlmsgrp  21236  rng2idl1cntr  21295  xrsmcmn  21381  cnfldexp  21394  cnmsubglem  21420  expmhm  21426  nn0srg  21427  rge0srg  21428  expghm  21465  fermltlchr  21519  freshmansdream  21564  frobrhm  21565  cnmsgnbas  21568  sraassab  21858  assamulgscmlem1  21889  assamulgscmlem2  21890  psrcrng  21960  mplcoe3  22026  mplcoe5lem  22027  mplcoe5  22028  mplbas2  22030  evlslem3  22068  evlslem6  22069  evlslem1  22070  evlsvvvallem  22079  evlsvvval  22081  evlsgsummul  22085  evlspw  22086  mpfind  22103  mhppwdeg  22126  psdpw  22146  ply1moncl  22246  coe1tm  22248  coe1pwmul  22254  ply1scltm  22256  ply1idvr1  22269  ply1coefsupp  22272  ply1coe  22273  gsummoncoe1  22283  lply1binomsc  22286  ply1fermltlchr  22287  evls1gsummul  22300  evls1pw  22301  evl1expd  22320  evl1gsummul  22335  evl1scvarpw  22338  evl1scvarpwval  22339  evl1gsummon  22340  evls1fpws  22344  rhmply1mon  22364  ringvcl  22375  mamuvs2  22381  matgsumcl  22435  madetsmelbas  22439  madetsmelbas2  22440  mat1mhm  22459  scmatmhm  22509  mdetleib2  22563  mdetf  22570  m1detdiag  22572  mdetdiaglem  22573  mdetdiag  22574  mdetdiagid  22575  mdetrlin  22577  mdetrsca  22578  mdetralt  22583  mdetunilem7  22593  mdetunilem8  22594  mdetuni0  22596  m2detleiblem2  22603  m2detleiblem3  22604  m2detleiblem4  22605  smadiadetlem4  22644  mat2pmatmhm  22708  pmatcollpwscmatlem1  22764  mply1topmatcllem  22778  mply1topmatcl  22780  pm2mpghm  22791  pm2mpmhm  22795  monmat2matmon  22799  pm2mp  22800  chpscmat  22817  chpscmatgsumbin  22819  chpscmatgsummon  22820  chp0mat  22821  chpidmat  22822  chfacfscmulcl  22832  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmulcl  22836  chfacfpmmul0  22837  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  cayhamlem2  22859  cayhamlem4  22863  nrgtrg  24665  deg1pw  26096  ply1remlem  26140  fta1blem  26146  idomrootle  26148  plypf1  26187  efabl  26527  efsubm  26528  amgm  26968  wilthlem2  27046  wilthlem3  27047  dchrelbas2  27214  dchrelbas3  27215  dchrzrhmul  27223  dchrmulcl  27226  dchrn0  27227  dchrinvcl  27230  dchrfi  27232  dchrsum2  27245  sum2dchr  27251  lgsqrlem1  27323  lgsqrlem2  27324  lgsqrlem3  27325  lgsqrlem4  27326  lgseisenlem3  27354  lgseisenlem4  27355  dchrisum0flblem1  27485  zsoring  28415  cntrcrng  33157  psgnid  33173  cnmsgn0g  33222  altgnsg  33225  urpropd  33307  ringm1expp1  33310  isunit3  33317  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrgspn  33322  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  0ringcring  33328  erlbr2d  33340  erler  33341  rlocaddval  33344  rlocmulval  33345  rloccring  33346  rloc0g  33347  rloc1r  33348  rlocf1  33349  domnprodn0  33351  domnprodeq0  33352  rrgsubm  33360  znfermltl  33441  unitprodclb  33464  elringlsm  33468  ringlsmss  33470  lsmsnpridl  33473  cringm4  33521  ssdifidlprm  33533  mxidlprm  33545  rprmdvdspow  33608  rprmdvdsprod  33609  1arithidomlem1  33610  1arithidom  33612  1arithufdlem1  33619  1arithufdlem2  33620  1arithufdlem3  33621  1arithufdlem4  33622  dfufd2lem  33624  zringfrac  33629  ressply1evls1  33640  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  evls1monply1  33654  deg1prod  33658  ply1coedeg  33664  coe1vr1  33666  deg1vr  33667  gsummoncoe1fzo  33672  evlextv  33701  psrmonprod  33711  mplmonprod  33713  vietalem  33738  vieta  33739  srapwov  33748  ply1degltdimlem  33782  ply1degltdim  33783  assarrginv  33796  evls1fldgencl  33830  extdgfialglem1  33852  extdgfialglem2  33853  rtelextdg2lem  33886  2sqr3minply  33940  cos9thpiminplylem6  33947  cos9thpiminply  33948  mdetpmtr1  33983  iistmd  34062  xrge0iifmhm  34099  xrge0pluscn  34100  pl1cn  34115  zrhcntr  34139  aks6d1c1p2  42562  aks6d1c1p3  42563  aks6d1c1p4  42564  aks6d1c1p5  42565  aks6d1c1p7  42566  aks6d1c1p6  42567  aks6d1c1p8  42568  aks6d1c1  42569  evl1gprodd  42570  aks6d1c2lem4  42580  idomnnzpownz  42585  idomnnzgmulnz  42586  ringexp0nn  42587  aks6d1c5lem0  42588  aks6d1c5lem3  42590  aks6d1c5lem2  42591  aks6d1c5  42592  deg1gprod  42593  deg1pow  42594  aks6d1c6lem1  42623  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks5lem2  42640  aks5lem3a  42642  unitscyglem5  42652  aks5lem7  42653  domnexpgn0cl  42982  abvexp  42991  fidomncyc  42994  evlsexpval  43017  selvvvval  43032  evlselv  43034  mhphf  43044  hbtlem4  43572  mon1psubm  43645  deg1mhm  43646  amgm2d  44643  amgm3d  44644  amgm4d  44645  2zrngmmgm  48740  2zrngmsgrp  48741  2zrngnring  48746  cznrng  48749  cznnring  48750  mgpsumunsn  48849  mgpsumz  48850  mgpsumn  48851  invginvrid  48855  ply1vr1smo  48871  ply1mulgsumlem4  48877  ply1mulgsum  48878  elmgpcntrd  49492  amgmlemALT  50290  amgmw2d  50291