MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mgpbas Structured version   Unicode version

Theorem mgpbas 16720
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  |-  M  =  (mulGrp `  R )
mgpbas.2  |-  B  =  ( Base `  R
)
Assertion
Ref Expression
mgpbas  |-  B  =  ( Base `  M
)

Proof of Theorem mgpbas
StepHypRef Expression
1 mgpbas.2 . 2  |-  B  =  ( Base `  R
)
2 mgpbas.1 . . 3  |-  M  =  (mulGrp `  R )
3 df-base 14298 . . 3  |-  Base  = Slot  1
4 1nn 10445 . . 3  |-  1  e.  NN
5 1ne2 10646 . . 3  |-  1  =/=  2
62, 3, 4, 5mgplem 16719 . 2  |-  ( Base `  R )  =  (
Base `  M )
71, 6eqtri 2483 1  |-  B  =  ( Base `  M
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   ` cfv 5527   1c1 9395   Basecbs 14293  mulGrpcmgp 16714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-cnex 9450  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470  ax-pre-mulgt0 9471
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-tr 4495  df-eprel 4741  df-id 4745  df-po 4750  df-so 4751  df-fr 4788  df-we 4790  df-ord 4831  df-on 4832  df-lim 4833  df-suc 4834  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-om 6588  df-recs 6943  df-rdg 6977  df-er 7212  df-en 7422  df-dom 7423  df-sdom 7424  df-pnf 9532  df-mnf 9533  df-xr 9534  df-ltxr 9535  df-le 9536  df-sub 9709  df-neg 9710  df-nn 10435  df-2 10492  df-ndx 14296  df-slot 14297  df-base 14298  df-sets 14299  df-plusg 14371  df-mgp 16715
This theorem is referenced by:  mgptopn  16723  mgpress  16725  dfur2  16729  srgcl  16737  srgass  16738  srgideu  16739  srgidcl  16742  srgidmlem  16744  issrgid  16747  srgpcomp  16754  srgpcompp  16755  srgpcomppsc  16756  srgbinomlem1  16762  srgbinomlem4  16765  srgbinomlem  16766  srgbinom  16767  csrgbinom  16768  rngcl  16782  crngcom  16783  iscrng2  16784  rngass  16785  rngideu  16786  rngidcl  16789  rngidmlem  16791  isrngid  16794  rngidss  16795  rngpropd  16800  crngpropd  16801  isrngd  16803  iscrngd  16804  gsummgp0  16823  prdsmgp  16826  oppr1  16850  unitgrpbas  16882  unitsubm  16886  rngidpropd  16911  dfrhm2  16932  rhmmul  16941  isrhm2d  16942  rhmf1o  16945  pwsco1rhm  16950  pwsco2rhm  16951  isdrng2  16966  drngmcl  16969  drngid2  16972  isdrngd  16981  subrgsubm  17002  issubrg3  17017  cntzsubr  17021  pwsdiagrhm  17022  rhmpropd  17024  rlmscaf  17413  sraassa  17520  psrcrng  17610  mplcoe3  17670  mplcoe3OLD  17671  mplcoe5lem  17672  mplcoe5  17673  mplcoe2OLD  17675  mplbas2  17676  mplbas2OLD  17677  evlslem6  17723  evlslem6OLD  17724  evlslem3  17725  evlslem1  17726  mpfind  17747  ply1moncl  17849  coe1tm  17851  coe1pwmul  17857  ply1scltm  17859  ply1coefsupp  17871  ply1coe  17872  ply1coeOLD  17873  evls1gsummul  17886  evls1varpw  17887  evl1expd  17905  evl1gsummul  17920  evl1scvarpw  17923  evl1scvarpwval  17924  evl1gsummon  17925  xrsmcmn  17965  cnfldexp  17975  cnmsubglem  18001  expmhm  18006  nn0srg  18007  rge0srg  18008  expghm  18049  expghmOLD  18050  cnmsgnbas  18134  rngvcl  18424  mamuvs2  18436  matgsumcl  18473  madetsmelbas  18477  madetsmelbas2  18478  mdetleib2  18527  mdetf  18534  m1detdiag  18536  mdetdiaglem  18537  mdetdiag  18538  mdetdiagid  18539  mdetrlin  18541  mdetrsca  18542  mdetralt  18547  mdetunilem7  18557  mdetunilem8  18558  mdetuni0  18560  m2detleiblem2  18567  m2detleiblem3  18568  m2detleiblem4  18569  smadiadetlem4  18608  nrgtrg  20403  deg1pwle  21725  deg1pw  21726  ply1remlem  21768  fta1blem  21774  plypf1  21814  amgm  22518  wilthlem2  22541  wilthlem3  22542  dchrelbas2  22710  dchrelbas3  22711  dchrzrhmul  22719  dchrmulcl  22722  dchrn0  22723  dchrinvcl  22726  dchrfi  22728  dchrsum2  22741  sum2dchr  22747  lgsqrlem1  22814  lgsqrlem2  22815  lgsqrlem3  22816  lgsqrlem4  22817  lgseisenlem3  22824  lgseisenlem4  22825  dchrisum0flblem1  22891  iistmd  26478  xrge0iifmhm  26515  xrge0pluscn  26516  pl1cn  26531  hbtlem4  29631  subrgacs  29706  cntzsdrg  29708  idomrootle  29709  isdomn3  29721  mon1psubm  29723  deg1mhm  29724  mgpsumunsn  30908  mgpsumz  30909  mgpsumn  30910  invginvrid  30921  assamulgscmlem1  30976  assamulgscmlem2  30977  ply1vr1smo  30980  mon1ply1  30994  gsummoncoe1  30997  ply1mulgsumlem4  31002  ply1mulgsum  31003  lply1binomsc  31011  rng1  31158  mat2pmatmhm  31223  pmatcollpwscmatlem1  31277  mply1topmatcllem  31291  mply1topmatcl  31293  pm2mpghm  31304  pm2mpmhm  31308  monmat2matmon  31311  pm2mp  31312  cpscmat  31329  cpscmatgsumbin  31331  cpscmatgsummon  31332  cp0mat  31333  cpidmat  31334  chfacfscmulcl  31344  chfacfscmul0  31345  chfacfscmulgsum  31347  chfacfpmmulcl  31348  chfacfpmmul0  31349  chfacfpmmulgsum  31351  chfacfpmmulgsum2  31352  cayhamlem1  31353  cpmadugsumlemB  31361  cpmadugsumlemC  31362  cpmadugsumlemF  31363  cayhamlem2  31372  cayhamlem4  31376
  Copyright terms: Public domain W3C validator