Theorem mgpbas 20084

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

Syntax hints:   = wceq 1542  ‘cfv 6490  Basecbs 17137  ._rcmulr 17179  mulGrpcmgp 20079

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 5300  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104

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 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-xr 11171  df-ltxr 11172  df-le 11173  df-sub 11367  df-neg 11368  df-nn 12147  df-2 12209  df-sets 17092  df-slot 17110  df-ndx 17122  df-base 17138  df-plusg 17191  df-mgp 20080

This theorem is referenced by:  mgptopn  20087  mgpress  20089  prdsmgp  20090  rngass  20098  rngcl  20103  isrngd  20112  rngpropd  20113  dfur2  20123  srgcl  20132  srgass  20133  srgideu  20134  srgidcl  20138  srgidmlem  20140  issrgid  20143  srg1zr  20154  srgpcomp  20157  srgpcompp  20158  srgpcomppsc  20159  srgbinomlem1  20165  srgbinomlem4  20168  srgbinomlem  20169  srgbinom  20170  csrgbinom  20171  ringcl  20189  crngcom  20190  iscrng2  20191  ringass  20192  ringideu  20193  crngbascntr  20195  ringidcl  20204  ringidmlem  20207  isringid  20210  ringidss  20216  isringrng  20226  ringpropd  20227  crngpropd  20228  isringd  20230  iscrngd  20231  ring1  20249  gsummgp0  20255  pwspjmhmmgpd  20265  pwsexpg  20266  pwsgprod  20267  xpsring1d  20271  oppr1  20288  unitgrpbas  20320  unitsubm  20324  rngidpropd  20353  isrnghmmul  20380  rnghmf1o  20390  idrnghm  20396  dfrhm2  20412  rhmmul  20423  isrhm2d  20424  idrhm  20427  rhmf1o  20428  pwsco1rhm  20437  pwsco2rhm  20438  c0rhm  20469  c0rnghm  20470  rhmimasubrnglem  20500  rhmimasubrng  20501  cntzsubrng  20502  subrgsubm  20520  issubrg3  20535  cntzsubr  20541  pwsdiagrhm  20542  rhmpropd  20544  isdomn3  20650  isdrng2  20678  drngmclOLD  20686  drngid2  20687  isdrngd  20700  isdrngdOLD  20702  subrgacs  20735  cntzsdrg  20737  subdrgint  20738  primefld  20740  rlmscaf  21161  rnglidlmmgm  21202  rnglidlmsgrp  21203  rng2idl1cntr  21262  xrsmcmn  21348  cnfldexp  21361  cnmsubglem  21387  expmhm  21393  nn0srg  21394  rge0srg  21395  expghm  21432  fermltlchr  21486  freshmansdream  21531  frobrhm  21532  cnmsgnbas  21535  sraassab  21825  assamulgscmlem1  21856  assamulgscmlem2  21857  psrcrng  21928  mplcoe3  21994  mplcoe5lem  21995  mplcoe5  21996  mplbas2  21998  evlslem3  22036  evlslem6  22037  evlslem1  22038  evlsvvvallem  22047  evlsvvval  22049  evlsgsummul  22053  evlspw  22054  mpfind  22071  mhppwdeg  22094  psdpw  22114  ply1moncl  22214  coe1tm  22216  coe1pwmul  22222  ply1scltm  22224  ply1idvr1  22237  ply1coefsupp  22240  ply1coe  22241  gsummoncoe1  22251  lply1binomsc  22254  ply1fermltlchr  22255  evls1gsummul  22268  evls1pw  22269  evl1expd  22288  evl1gsummul  22303  evl1scvarpw  22306  evl1scvarpwval  22307  evl1gsummon  22308  evls1fpws  22312  rhmply1mon  22332  ringvcl  22343  mamuvs2  22349  matgsumcl  22403  madetsmelbas  22407  madetsmelbas2  22408  mat1mhm  22427  scmatmhm  22477  mdetleib2  22531  mdetf  22538  m1detdiag  22540  mdetdiaglem  22541  mdetdiag  22542  mdetdiagid  22543  mdetrlin  22545  mdetrsca  22546  mdetralt  22551  mdetunilem7  22561  mdetunilem8  22562  mdetuni0  22564  m2detleiblem2  22571  m2detleiblem3  22572  m2detleiblem4  22573  smadiadetlem4  22612  mat2pmatmhm  22676  pmatcollpwscmatlem1  22732  mply1topmatcllem  22746  mply1topmatcl  22748  pm2mpghm  22759  pm2mpmhm  22763  monmat2matmon  22767  pm2mp  22768  chpscmat  22785  chpscmatgsumbin  22787  chpscmatgsummon  22788  chp0mat  22789  chpidmat  22790  chfacfscmulcl  22800  chfacfscmul0  22801  chfacfscmulgsum  22803  chfacfpmmulcl  22804  chfacfpmmul0  22805  chfacfpmmulgsum  22807  chfacfpmmulgsum2  22808  cayhamlem1  22809  cpmadugsumlemB  22817  cpmadugsumlemC  22818  cpmadugsumlemF  22819  cayhamlem2  22827  cayhamlem4  22831  nrgtrg  24633  deg1pw  26067  ply1remlem  26111  fta1blem  26117  idomrootle  26119  plypf1  26158  efabl  26499  efsubm  26500  amgm  26941  wilthlem2  27019  wilthlem3  27020  dchrelbas2  27188  dchrelbas3  27189  dchrzrhmul  27197  dchrmulcl  27200  dchrn0  27201  dchrinvcl  27204  dchrfi  27206  dchrsum2  27219  sum2dchr  27225  lgsqrlem1  27297  lgsqrlem2  27298  lgsqrlem3  27299  lgsqrlem4  27300  lgseisenlem3  27328  lgseisenlem4  27329  dchrisum0flblem1  27459  zsoring  28389  cntrcrng  33147  psgnid  33163  cnmsgn0g  33212  altgnsg  33215  urpropd  33297  ringm1expp1  33300  isunit3  33307  elrgspnlem1  33308  elrgspnlem2  33309  elrgspnlem3  33310  elrgspnlem4  33311  elrgspn  33312  elrgspnsubrunlem1  33313  elrgspnsubrunlem2  33314  0ringcring  33318  erlbr2d  33330  erler  33331  rlocaddval  33334  rlocmulval  33335  rloccring  33336  rloc0g  33337  rloc1r  33338  rlocf1  33339  domnprodn0  33341  domnprodeq0  33342  rrgsubm  33350  znfermltl  33431  unitprodclb  33454  elringlsm  33458  ringlsmss  33460  lsmsnpridl  33463  cringm4  33511  ssdifidlprm  33523  mxidlprm  33535  rprmdvdspow  33598  rprmdvdsprod  33599  1arithidomlem1  33600  1arithidom  33602  1arithufdlem1  33609  1arithufdlem2  33610  1arithufdlem3  33611  1arithufdlem4  33612  dfufd2lem  33614  zringfrac  33619  ressply1evls1  33630  evl1deg1  33641  evl1deg2  33642  evl1deg3  33643  evls1monply1  33644  deg1prod  33648  ply1coedeg  33654  coe1vr1  33656  deg1vr  33657  gsummoncoe1fzo  33662  evlextv  33691  psrmonprod  33701  mplmonprod  33703  vietalem  33728  vieta  33729  srapwov  33738  ply1degltdimlem  33772  ply1degltdim  33773  assarrginv  33786  evls1fldgencl  33820  extdgfialglem1  33842  extdgfialglem2  33843  rtelextdg2lem  33876  2sqr3minply  33930  cos9thpiminplylem6  33937  cos9thpiminply  33938  mdetpmtr1  33973  iistmd  34052  xrge0iifmhm  34089  xrge0pluscn  34090  pl1cn  34105  zrhcntr  34129  aks6d1c1p2  42540  aks6d1c1p3  42541  aks6d1c1p4  42542  aks6d1c1p5  42543  aks6d1c1p7  42544  aks6d1c1p6  42545  aks6d1c1p8  42546  aks6d1c1  42547  evl1gprodd  42548  aks6d1c2lem4  42558  idomnnzpownz  42563  idomnnzgmulnz  42564  ringexp0nn  42565  aks6d1c5lem0  42566  aks6d1c5lem3  42568  aks6d1c5lem2  42569  aks6d1c5  42570  deg1gprod  42571  deg1pow  42572  aks6d1c6lem1  42601  aks6d1c6lem2  42602  aks6d1c6lem3  42603  aks5lem2  42618  aks5lem3a  42620  unitscyglem5  42630  aks5lem7  42631  domnexpgn0cl  42967  abvexp  42976  fidomncyc  42979  evlsexpval  43002  selvvvval  43017  evlselv  43019  mhphf  43029  hbtlem4  43557  mon1psubm  43630  deg1mhm  43631  amgm2d  44628  amgm3d  44629  amgm4d  44630  2zrngmmgm  48686  2zrngmsgrp  48687  2zrngnring  48692  cznrng  48695  cznnring  48696  mgpsumunsn  48795  mgpsumz  48796  mgpsumn  48797  invginvrid  48801  ply1vr1smo  48817  ply1mulgsumlem4  48823  ply1mulgsum  48824  elmgpcntrd  49438  amgmlemALT  50236  amgmw2d  50237