Theorem mgpbas 20124

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

Syntax hints:   = wceq 1547  ‘cfv 6492  Basecbs 17177  ._rcmulr 17219  mulGrpcmgp 20119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-2 12242  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-plusg 17231  df-mgp 20120

This theorem is referenced by:  mgptopn  20127  mgpress  20129  prdsmgp  20130  rngass  20138  rngcl  20143  isrngd  20152  rngpropd  20153  dfur2  20163  srgcl  20172  srgass  20173  srgideu  20174  srgidcl  20178  srgidmlem  20180  issrgid  20183  srg1zr  20194  srgpcomp  20197  srgpcompp  20198  srgpcomppsc  20199  srgbinomlem1  20205  srgbinomlem4  20208  srgbinomlem  20209  srgbinom  20210  csrgbinom  20211  ringcl  20229  crngcom  20230  iscrng2  20231  ringass  20232  ringideu  20233  crngbascntr  20235  ringidcl  20244  ringidmlem  20247  isringid  20250  ringidss  20256  isringrng  20266  ringpropd  20267  crngpropd  20268  isringd  20270  iscrngd  20271  ring1  20289  gsummgp0  20295  pwspjmhmmgpd  20305  pwsexpg  20306  pwsgprod  20307  xpsring1d  20311  oppr1  20328  unitgrpbas  20360  unitsubm  20364  rngidpropd  20393  isrnghmmul  20420  rnghmf1o  20430  idrnghm  20436  dfrhm2  20452  rhmmul  20464  isrhm2d  20465  idrhm  20468  rhmf1o  20469  pwsco1rhm  20480  pwsco2rhm  20481  c0rhm  20513  c0rnghm  20514  rhmimasubrnglem  20544  rhmimasubrng  20545  cntzsubrng  20546  subrgsubm  20564  issubrg3  20579  cntzsubr  20585  pwsdiagrhm  20586  rhmpropd  20588  isdomn3  20694  isdrng2  20722  drngmclOLD  20730  drngid2  20731  isdrngd  20744  isdrngdOLD  20746  subrgacs  20779  cntzsdrg  20781  subdrgint  20782  primefld  20784  rlmscaf  21204  rnglidlmmgm  21245  rnglidlmsgrp  21246  rng2idl1cntr  21305  xrsmcmn  21377  cnfldexp  21387  cnmsubglem  21412  expmhm  21418  nn0srg  21419  rge0srg  21420  expghm  21457  fermltlchr  21511  freshmansdream  21556  frobrhm  21557  cnmsgnbas  21560  sraassab  21850  assamulgscmlem1  21881  assamulgscmlem2  21882  psrcrng  21953  mplcoe3  22021  mplcoe5lem  22022  mplcoe5  22023  mplbas2  22025  evlslem3  22063  evlslem6  22064  evlslem1  22065  evlsvvvallem  22074  evlsvvval  22076  evlsgsummul  22080  evlspw  22081  mpfind  22098  evlsexpval  22111  selvvvval  22125  mhppwdeg  22145  psdpw  22165  ply1moncl  22264  coe1tm  22266  coe1pwmul  22272  ply1scltm  22274  ply1idvr1  22287  ply1coefsupp  22290  ply1coe  22291  gsummoncoe1  22301  lply1binomsc  22304  ply1fermltlchr  22305  evls1gsummul  22318  evls1pw  22319  evl1expd  22338  evl1gsummul  22353  evl1scvarpw  22356  evl1scvarpwval  22357  evl1gsummon  22358  evls1fpws  22362  rhmply1mon  22379  ringvcl  22390  mamuvs2  22396  matgsumcl  22450  madetsmelbas  22454  madetsmelbas2  22455  mat1mhm  22474  scmatmhm  22524  mdetleib2  22578  mdetf  22585  m1detdiag  22587  mdetdiaglem  22588  mdetdiag  22589  mdetdiagid  22590  mdetrlin  22592  mdetrsca  22593  mdetralt  22598  mdetunilem7  22608  mdetunilem8  22609  mdetuni0  22611  m2detleiblem2  22618  m2detleiblem3  22619  m2detleiblem4  22620  smadiadetlem4  22659  mat2pmatmhm  22723  pmatcollpwscmatlem1  22779  mply1topmatcllem  22793  mply1topmatcl  22795  pm2mpghm  22806  pm2mpmhm  22810  monmat2matmon  22814  pm2mp  22815  chpscmat  22832  chpscmatgsumbin  22834  chpscmatgsummon  22835  chp0mat  22836  chpidmat  22837  chfacfscmulcl  22847  chfacfscmul0  22848  chfacfscmulgsum  22850  chfacfpmmulcl  22851  chfacfpmmul0  22852  chfacfpmmulgsum  22854  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  cayhamlem2  22874  cayhamlem4  22878  nrgtrg  24680  deg1pw  26111  ply1remlem  26155  fta1blem  26161  idomrootle  26163  plypf1  26202  efabl  26539  efsubm  26540  amgm  26979  wilthlem2  27057  wilthlem3  27058  dchrelbas2  27225  dchrelbas3  27226  dchrzrhmul  27234  dchrmulcl  27237  dchrn0  27238  dchrinvcl  27241  dchrfi  27243  dchrsum2  27256  sum2dchr  27262  lgsqrlem1  27334  lgsqrlem2  27335  lgsqrlem3  27336  lgsqrlem4  27337  lgseisenlem3  27365  lgseisenlem4  27366  dchrisum0flblem1  27496  zsoring  28426  cntrcrng  33169  psgnid  33185  cnmsgn0g  33234  altgnsg  33237  urpropd  33319  ringm1expp1  33322  isunit3  33329  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  elrgspn  33334  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  0ringcring  33340  erlbr2d  33352  erler  33353  rlocaddval  33356  rlocmulval  33357  rloccring  33358  rloc0g  33359  rloc1r  33360  rlocf1  33361  domnprodn0  33363  domnprodeq0  33364  rrgsubm  33372  znfermltl  33456  unitprodclb  33479  elringlsm  33483  ringlsmss  33485  lsmsnpridl  33488  cringm4  33536  ssdifidlprm  33548  mxidlprm  33560  rprmdvdspow  33623  rprmdvdsprod  33624  1arithidomlem1  33625  1arithidom  33627  1arithufdlem1  33634  1arithufdlem2  33635  1arithufdlem3  33636  1arithufdlem4  33637  dfufd2lem  33639  zringfrac  33644  ressply1evls1  33655  evl1deg1  33666  evl1deg2  33667  evl1deg3  33668  evls1monply1  33669  deg1prod  33673  ply1coedeg  33679  coe1vr1  33681  deg1vr  33682  gsummoncoe1fzo  33687  evlextv  33733  psrmonprod  33743  mplmonprod  33745  vietalem  33770  vieta  33771  srapwov  33780  ply1degltdimlem  33813  ply1degltdim  33814  assarrginv  33827  evls1fldgencl  33861  extdgfialglem1  33883  extdgfialglem2  33884  rtelextdg2lem  33917  2sqr3minply  33971  cos9thpiminplylem6  33978  cos9thpiminply  33979  mdetpmtr1  34014  iistmd  34093  xrge0iifmhm  34130  xrge0pluscn  34131  pl1cn  34146  zrhcntr  34170  aks6d1c1p2  42601  aks6d1c1p3  42602  aks6d1c1p4  42603  aks6d1c1p5  42604  aks6d1c1p7  42605  aks6d1c1p6  42606  aks6d1c1p8  42607  aks6d1c1  42608  evl1gprodd  42609  aks6d1c2lem4  42619  idomnnzpownz  42624  idomnnzgmulnz  42625  ringexp0nn  42626  aks6d1c5lem0  42627  aks6d1c5lem3  42629  aks6d1c5lem2  42630  aks6d1c5  42631  deg1gprod  42632  deg1pow  42633  aks6d1c6lem1  42662  aks6d1c6lem2  42663  aks6d1c6lem3  42664  aks5lem2  42679  aks5lem3a  42681  unitscyglem5  42691  aks5lem7  42692  domnexpgn0cl  43016  abvexp  43025  fidomncyc  43028  evlselv  43046  mhphf  43054  hbtlem4  43578  mon1psubm  43651  deg1mhm  43652  amgm2d  44649  amgm3d  44650  amgm4d  44651  2zrngmmgm  48750  2zrngmsgrp  48751  2zrngnring  48756  cznrng  48759  cznnring  48760  mgpsumunsn  48859  mgpsumz  48860  mgpsumn  48861  invginvrid  48865  ply1vr1smo  48881  ply1mulgsumlem4  48887  ply1mulgsum  48888  elmgpcntrd  49502  amgmlemALT  50300  amgmw2d  50301