Theorem mgpbas 20111

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 2734	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20109	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17233	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17304	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19338	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2757	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1539  ‘cfv 6541  Basecbs 17230  ._rcmulr 17275  mulGrpcmgp 20106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-2 12311  df-sets 17184  df-slot 17202  df-ndx 17214  df-base 17231  df-plusg 17287  df-mgp 20107

This theorem is referenced by:  mgptopn  20114  mgpress  20116  prdsmgp  20117  rngass  20125  rngcl  20130  isrngd  20139  rngpropd  20140  dfur2  20150  srgcl  20159  srgass  20160  srgideu  20161  srgidcl  20165  srgidmlem  20167  issrgid  20170  srg1zr  20181  srgpcomp  20184  srgpcompp  20185  srgpcomppsc  20186  srgbinomlem1  20192  srgbinomlem4  20195  srgbinomlem  20196  srgbinom  20197  csrgbinom  20198  ringcl  20216  crngcom  20217  iscrng2  20218  ringass  20219  ringideu  20220  crngbascntr  20222  ringidcl  20231  ringidmlem  20234  isringid  20237  ringidss  20243  isringrng  20253  ringpropd  20254  crngpropd  20255  isringd  20257  iscrngd  20258  ring1  20276  gsummgp0  20284  pwspjmhmmgpd  20294  pwsexpg  20295  xpsring1d  20299  oppr1  20319  unitgrpbas  20351  unitsubm  20355  rngidpropd  20384  isrnghmmul  20411  rnghmf1o  20421  idrnghm  20427  dfrhm2  20443  rhmmul  20455  isrhm2d  20456  idrhm  20459  rhmf1o  20460  pwsco1rhm  20471  pwsco2rhm  20472  c0rhm  20503  c0rnghm  20504  rhmimasubrnglem  20534  rhmimasubrng  20535  cntzsubrng  20536  subrgsubm  20554  issubrg3  20569  cntzsubr  20575  pwsdiagrhm  20576  rhmpropd  20578  isdomn3  20684  isdrng2  20712  drngmclOLD  20720  drngid2  20721  isdrngd  20734  isdrngdOLD  20736  subrgacs  20770  cntzsdrg  20772  subdrgint  20773  primefld  20775  rlmscaf  21177  rnglidlmmgm  21218  rnglidlmsgrp  21219  rng2idl1cntr  21278  xrsmcmn  21367  cnfldexp  21380  cnmsubglem  21411  expmhm  21417  nn0srg  21418  rge0srg  21419  expghm  21449  fermltlchr  21503  freshmansdream  21548  frobrhm  21549  cnmsgnbas  21551  sraassab  21843  sraassaOLD  21845  assamulgscmlem1  21874  assamulgscmlem2  21875  psrcrng  21947  mplcoe3  22011  mplcoe5lem  22012  mplcoe5  22013  mplbas2  22015  evlslem3  22053  evlslem6  22054  evlslem1  22055  evlsgsummul  22065  evlspw  22066  mpfind  22080  mhppwdeg  22103  psdpw  22123  ply1moncl  22223  coe1tm  22225  coe1pwmul  22231  ply1scltm  22233  ply1idvr1  22247  ply1coefsupp  22250  ply1coe  22251  gsummoncoe1  22261  lply1binomsc  22264  ply1fermltlchr  22265  evls1gsummul  22278  evls1pw  22279  evl1expd  22298  evl1gsummul  22313  evl1scvarpw  22316  evl1scvarpwval  22317  evl1gsummon  22318  evls1fpws  22322  rhmply1mon  22342  ringvcl  22353  mamuvs2  22359  matgsumcl  22415  madetsmelbas  22419  madetsmelbas2  22420  mat1mhm  22439  scmatmhm  22489  mdetleib2  22543  mdetf  22550  m1detdiag  22552  mdetdiaglem  22553  mdetdiag  22554  mdetdiagid  22555  mdetrlin  22557  mdetrsca  22558  mdetralt  22563  mdetunilem7  22573  mdetunilem8  22574  mdetuni0  22576  m2detleiblem2  22583  m2detleiblem3  22584  m2detleiblem4  22585  smadiadetlem4  22624  mat2pmatmhm  22688  pmatcollpwscmatlem1  22744  mply1topmatcllem  22758  mply1topmatcl  22760  pm2mpghm  22771  pm2mpmhm  22775  monmat2matmon  22779  pm2mp  22780  chpscmat  22797  chpscmatgsumbin  22799  chpscmatgsummon  22800  chp0mat  22801  chpidmat  22802  chfacfscmulcl  22812  chfacfscmul0  22813  chfacfscmulgsum  22815  chfacfpmmulcl  22816  chfacfpmmul0  22817  chfacfpmmulgsum  22819  chfacfpmmulgsum2  22820  cayhamlem1  22821  cpmadugsumlemB  22829  cpmadugsumlemC  22830  cpmadugsumlemF  22831  cayhamlem2  22839  cayhamlem4  22843  nrgtrg  24648  deg1pw  26097  ply1remlem  26141  fta1blem  26147  idomrootle  26149  plypf1  26188  efabl  26529  efsubm  26530  amgm  26971  wilthlem2  27049  wilthlem3  27050  dchrelbas2  27218  dchrelbas3  27219  dchrzrhmul  27227  dchrmulcl  27230  dchrn0  27231  dchrinvcl  27234  dchrfi  27236  dchrsum2  27249  sum2dchr  27255  lgsqrlem1  27327  lgsqrlem2  27328  lgsqrlem3  27329  lgsqrlem4  27330  lgseisenlem3  27358  lgseisenlem4  27359  dchrisum0flblem1  27489  cntrcrng  33017  psgnid  33061  cnmsgn0g  33110  altgnsg  33113  urpropd  33180  isunit3  33189  elrgspnlem1  33190  elrgspnlem2  33191  elrgspnlem3  33192  elrgspnlem4  33193  elrgspn  33194  elrgspnsubrunlem1  33195  elrgspnsubrunlem2  33196  0ringcring  33200  erlbr2d  33212  erler  33213  rlocaddval  33216  rlocmulval  33217  rloccring  33218  rloc0g  33219  rloc1r  33220  rlocf1  33221  domnprodn0  33223  rrgsubm  33231  znfermltl  33334  unitprodclb  33357  elringlsm  33361  ringlsmss  33363  lsmsnpridl  33366  cringm4  33414  ssdifidlprm  33426  mxidlprm  33438  rprmdvdspow  33501  rprmdvdsprod  33502  1arithidomlem1  33503  1arithidom  33505  1arithufdlem1  33512  1arithufdlem2  33513  1arithufdlem3  33514  1arithufdlem4  33515  dfufd2lem  33517  zringfrac  33522  evl1deg1  33541  evl1deg2  33542  evl1deg3  33543  coe1vr1  33553  deg1vr  33554  gsummoncoe1fzo  33558  ply1degltdimlem  33613  ply1degltdim  33614  assarrginv  33627  evls1fldgencl  33662  rtelextdg2lem  33711  2sqr3minply  33765  mdetpmtr1  33797  iistmd  33876  xrge0iifmhm  33913  xrge0pluscn  33914  pl1cn  33929  zrhcntr  33955  aks6d1c1p2  42085  aks6d1c1p3  42086  aks6d1c1p4  42087  aks6d1c1p5  42088  aks6d1c1p7  42089  aks6d1c1p6  42090  aks6d1c1p8  42091  aks6d1c1  42092  evl1gprodd  42093  aks6d1c2lem4  42103  idomnnzpownz  42108  idomnnzgmulnz  42109  ringexp0nn  42110  aks6d1c5lem0  42111  aks6d1c5lem3  42113  aks6d1c5lem2  42114  aks6d1c5  42115  deg1gprod  42116  deg1pow  42117  aks6d1c6lem1  42146  aks6d1c6lem2  42147  aks6d1c6lem3  42148  aks5lem2  42163  aks5lem3a  42165  unitscyglem5  42175  aks5lem7  42176  domnexpgn0cl  42512  abvexp  42521  fidomncyc  42524  pwsgprod  42533  evlsvvvallem  42550  evlsvvval  42552  evlsexpval  42556  selvvvval  42574  evlselv  42576  mhphf  42586  hbtlem4  43116  mon1psubm  43189  deg1mhm  43190  amgm2d  44188  amgm3d  44189  amgm4d  44190  2zrngmmgm  48141  2zrngmsgrp  48142  2zrngnring  48147  cznrng  48150  cznnring  48151  mgpsumunsn  48250  mgpsumz  48251  mgpsumn  48252  invginvrid  48256  ply1vr1smo  48272  ply1mulgsumlem4  48279  ply1mulgsum  48280  elmgpcntrd  48886  amgmlemALT  49417  amgmw2d  49418