Theorem mgpbas 20222

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 2763	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20220	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17273	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17341	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19421	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2786	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1570  ‘cfv 6538  Basecbs 17270  ._rcmulr 17312  mulGrpcmgp 20217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-nn 12235  df-2 12304  df-sets 17225  df-slot 17243  df-ndx 17255  df-base 17271  df-plusg 17324  df-mgp 20218

This theorem is referenced by:  mgptopn  20225  mgpress  20227  prdsmgp  20228  elmgplsm  20229  rngass  20238  rngcl  20243  isrngd  20252  rngpropd  20253  rng1zrlem  20260  dfur2  20267  srgcl  20276  srgass  20277  srgideu  20278  srgidcl  20282  srgidmlem  20284  issrgid  20287  srgpcomp  20301  srgpcompp  20302  srgpcomppsc  20303  srgbinomlem1  20309  srgbinomlem4  20312  srgbinomlem  20313  srgbinom  20314  csrgbinom  20315  ringcl  20333  crngcom  20334  iscrng2  20335  ringass  20336  ringideu  20337  crngbascntr  20339  ringidcl  20349  ringidmlem  20352  isringid  20355  ringidss  20361  isringrng  20371  ringpropd  20372  crngpropd  20373  isringd  20375  iscrngd  20376  ring1  20394  gsummgp0  20400  pwspjmhmmgpd  20410  pwsexpg  20411  pwsgprod  20412  xpsring1d  20416  oppr1  20433  unitgrpbas  20465  unitsubm  20469  rngidpropd  20498  isrnghmmul  20525  rnghmf1o  20535  idrnghm  20541  dfrhm2  20557  rhmmul  20569  isrhm2d  20570  idrhm  20573  rhmf1o  20574  pwsco1rhm  20585  pwsco2rhm  20586  c0rhm  20620  c0rnghm  20621  rhmimasubrnglem  20651  rhmimasubrng  20652  cntzsubrng  20653  subrgsubm  20671  issubrg3  20686  cntzsubr  20692  pwsdiagrhm  20693  rhmpropd  20695  isdomn3  20800  isdrng2  20830  drngid2  20838  isdrngd  20850  isdrngdOLD  20852  subrgacs  20884  cntzsdrg  20886  subdrgint  20887  primefld  20889  rlmscaf  21309  rnglidlmmgm  21360  rnglidlmsgrp  21361  rng2idl1cntr  21426  cringm4  21452  ssdifidlprm  21467  prmidlsubm  21468  xrsmcmn  21526  cnfldexp  21536  cnmsubglem  21561  expmhm  21567  nn0srg  21568  rge0srg  21569  expghm  21606  fermltlchr  21660  freshmansdream  21705  frobrhm  21706  cnmsgnbas  21709  sraassab  21999  assamulgscmlem1  22030  assamulgscmlem2  22031  psrcrng  22102  mplcoe3  22170  mplcoe5lem  22171  mplcoe5  22172  mplbas2  22174  evlslem3  22212  evlslem6  22213  evlslem1  22214  evlsvvvallem  22223  evlsvvval  22225  evlsgsummul  22229  evlspw  22230  mpfind  22247  evlsexpval  22260  selvvvval  22274  mhppwdeg  22294  psdpw  22314  ply1moncl  22413  coe1tm  22415  coe1pwmul  22421  ply1scltm  22423  ply1idvr1  22436  ply1coefsupp  22438  ply1coe  22439  gsummoncoe1  22449  lply1binomsc  22452  ply1fermltlchr  22453  evls1gsummul  22466  evls1pw  22467  evl1expd  22486  evl1gsummul  22501  evl1scvarpw  22504  evl1scvarpwval  22505  evl1gsummon  22506  evls1fpws  22510  rhmply1mon  22527  ringvcl  22538  mamuvs2  22544  matgsumcl  22598  madetsmelbas  22602  madetsmelbas2  22603  mat1mhm  22622  scmatmhm  22672  mdetleib2  22726  mdetf  22733  m1detdiag  22735  mdetdiaglem  22736  mdetdiag  22737  mdetdiagid  22738  mdetrlin  22740  mdetrsca  22741  mdetralt  22746  mdetunilem7  22756  mdetunilem8  22757  mdetuni0  22759  m2detleiblem2  22766  m2detleiblem3  22767  m2detleiblem4  22768  smadiadetlem4  22807  mat2pmatmhm  22871  pmatcollpwscmatlem1  22927  mply1topmatcllem  22941  mply1topmatcl  22943  pm2mpghm  22954  pm2mpmhm  22958  monmat2matmon  22962  pm2mp  22963  chpscmat  22980  chpscmatgsumbin  22982  chpscmatgsummon  22983  chp0mat  22984  chpidmat  22985  chfacfscmulcl  22995  chfacfscmul0  22996  chfacfscmulgsum  22998  chfacfpmmulcl  22999  chfacfpmmul0  23000  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  cayhamlem2  23022  cayhamlem4  23026  nrgtrg  24828  deg1pw  26259  ply1remlem  26303  fta1blem  26309  idomrootle  26311  plypf1  26350  efabl  26696  efsubm  26697  amgm  27136  wilthlem2  27214  wilthlem3  27215  dchrelbas2  27382  dchrelbas3  27383  dchrzrhmul  27391  dchrmulcl  27394  dchrn0  27395  dchrinvcl  27398  dchrfi  27400  dchrsum2  27413  sum2dchr  27419  lgsqrlem1  27491  lgsqrlem2  27492  lgsqrlem3  27493  lgsqrlem4  27494  lgseisenlem3  27522  lgseisenlem4  27523  dchrisum0flblem1  27653  zsoring  28583  cntrcrng  33382  psgnid  33398  cnmsgn0g  33447  altgnsg  33450  urpropd  33531  ringm1expp1  33534  isunit3  33541  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem3  33545  elrgspnlem4  33546  elrgspn  33547  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  0ringcring  33553  erlbr2d  33565  erler  33566  erld2  33567  rlocaddval  33570  rlocmulval  33571  rloccring  33572  rloc0g  33573  rloc1r  33574  rlocf1  33575  rlocinvunit  33576  rlocisunit  33577  domnprodn0  33579  domnprodeq0  33580  rrgsubm  33585  znfermltl  33662  unitprodclb  33683  ringlsmss  33687  lsmsnpridl  33690  mxidlprm  33734  rprmdvdspow  33804  rprmdvdsprod  33805  1arithidomlem1  33806  1arithidom  33808  1arithufdlem1  33815  1arithufdlem2  33816  1arithufdlem3  33817  1arithufdlem4  33818  dfufd2lem  33820  zringfrac  33825  ressply1evls1  33836  evl1deg1  33847  evl1deg2  33848  evl1deg3  33849  evls1monply1  33850  deg1prod  33854  ply1coedeg  33860  coe1vr1  33862  deg1vr  33863  gsummoncoe1fzo  33868  evlextv  33913  psrmonprod  33923  mplmonprod  33925  vietalem  33950  vieta  33951  srapwov  33960  ply1degltdimlem  33993  ply1degltdim  33994  assarrginv  34007  evls1fldgencl  34041  extdgfialglem1  34063  extdgfialglem2  34064  rtelextdg2lem  34097  2sqr3minply  34151  cos9thpiminplylem6  34158  cos9thpiminply  34159  mdetpmtr1  34194  iistmd  34273  xrge0iifmhm  34310  xrge0pluscn  34311  pl1cn  34326  zrhcntr  34350  aks6d1c1p2  42857  aks6d1c1p3  42858  aks6d1c1p4  42859  aks6d1c1p5  42860  aks6d1c1p7  42861  aks6d1c1p6  42862  aks6d1c1p8  42863  aks6d1c1  42864  evl1gprodd  42865  aks6d1c2lem4  42875  idomnnzpownz  42880  idomnnzgmulnz  42881  ringexp0nn  42882  aks6d1c5lem0  42883  aks6d1c5lem3  42885  aks6d1c5lem2  42886  aks6d1c5  42887  deg1gprod  42888  deg1pow  42889  aks6d1c6lem1  42918  aks6d1c6lem2  42919  aks6d1c6lem3  42920  aks5lem2  42935  aks5lem3a  42937  unitscyglem5  42947  aks5lem7  42948  domnexpgn0cl  43274  abvexp  43283  fidomncyc  43286  evlselv  43304  mhphf  43312  hbtlem4  43836  mon1psubm  43909  deg1mhm  43910  amgm2d  44907  amgm3d  44908  amgm4d  44909  2zrngmmgm  49000  2zrngmsgrp  49001  2zrngnring  49006  cznrng  49009  cznnring  49010  mgpsumunsn  49124  mgpsumz  49125  mgpsumn  49126  invginvrid  49130  ply1vr1smo  49146  ply1mulgsumlem4  49152  ply1mulgsum  49153  elmgpcntrd  49766  amgmlemALT  50586  amgmw2d  50587