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

Theorem mgpbas 17778
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 15175 . . 3  |-  Base  = Slot  1
4 1nn 10648 . . 3  |-  1  e.  NN
5 1ne2 10851 . . 3  |-  1  =/=  2
62, 3, 4, 5mgplem 17777 . 2  |-  ( Base `  R )  =  (
Base `  M )
71, 6eqtri 2484 1  |-  B  =  ( Base `  M
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455   ` cfv 5601   1c1 9566   Basecbs 15170  mulGrpcmgp 17772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-plusg 15252  df-mgp 17773
This theorem is referenced by:  mgptopn  17781  mgpress  17783  dfur2  17787  srgcl  17795  srgass  17796  srgideu  17797  srgidcl  17800  srgidmlem  17802  issrgid  17805  srg1zr  17811  srgpcomp  17814  srgpcompp  17815  srgpcomppsc  17816  srgbinomlem1  17822  srgbinomlem4  17825  srgbinomlem  17826  srgbinom  17827  csrgbinom  17828  ringcl  17843  crngcom  17844  iscrng2  17845  ringass  17846  ringideu  17847  ringidcl  17850  ringidmlem  17852  isringid  17855  ringidss  17856  ringpropd  17861  crngpropd  17862  isringd  17864  iscrngd  17865  ring1  17879  gsummgp0  17885  prdsmgp  17887  oppr1  17911  unitgrpbas  17943  unitsubm  17947  rngidpropd  17972  dfrhm2  17994  rhmmul  18004  isrhm2d  18005  idrhm  18008  rhmf1o  18009  pwsco1rhm  18015  pwsco2rhm  18016  isdrng2  18034  drngmcl  18037  drngid2  18040  isdrngd  18049  subrgsubm  18070  issubrg3  18085  cntzsubr  18089  pwsdiagrhm  18090  rhmpropd  18092  rlmscaf  18480  sraassa  18598  assamulgscmlem1  18621  assamulgscmlem2  18622  psrcrng  18686  mplcoe3  18739  mplcoe5lem  18740  mplcoe5  18741  mplbas2  18743  evlslem6  18785  evlslem3  18786  evlslem1  18787  mpfind  18808  ply1moncl  18913  coe1tm  18915  coe1pwmul  18921  ply1scltm  18923  ply1coefsupp  18937  ply1coe  18938  ply1coeOLD  18939  gsummoncoe1  18947  lply1binomsc  18950  evls1gsummul  18963  evls1varpw  18964  evl1expd  18982  evl1gsummul  18997  evl1scvarpw  19000  evl1scvarpwval  19001  evl1gsummon  19002  xrsmcmn  19040  cnfldexp  19050  cnmsubglem  19079  expmhm  19085  nn0srg  19086  rge0srg  19087  expghm  19116  cnmsgnbas  19195  ringvcl  19472  mamuvs2  19480  matgsumcl  19534  madetsmelbas  19538  madetsmelbas2  19539  mat1mhm  19558  scmatmhm  19608  mdetleib2  19662  mdetf  19669  m1detdiag  19671  mdetdiaglem  19672  mdetdiag  19673  mdetdiagid  19674  mdetrlin  19676  mdetrsca  19677  mdetralt  19682  mdetunilem7  19692  mdetunilem8  19693  mdetuni0  19695  m2detleiblem2  19702  m2detleiblem3  19703  m2detleiblem4  19704  smadiadetlem4  19743  mat2pmatmhm  19806  pmatcollpwscmatlem1  19862  mply1topmatcllem  19876  mply1topmatcl  19878  pm2mpghm  19889  pm2mpmhm  19893  monmat2matmon  19897  pm2mp  19898  chpscmat  19915  chpscmatgsumbin  19917  chpscmatgsummon  19918  chp0mat  19919  chpidmat  19920  chfacfscmulcl  19930  chfacfscmul0  19931  chfacfscmulgsum  19933  chfacfpmmulcl  19934  chfacfpmmul0  19935  chfacfpmmulgsum  19937  chfacfpmmulgsum2  19938  cayhamlem1  19939  cpmadugsumlemB  19947  cpmadugsumlemC  19948  cpmadugsumlemF  19949  cayhamlem2  19957  cayhamlem4  19961  nrgtrg  21741  deg1pw  23118  ply1remlem  23162  fta1blem  23168  plypf1  23215  efabl  23548  efsubm  23549  amgm  23965  wilthlem2  24043  wilthlem3  24044  dchrelbas2  24214  dchrelbas3  24215  dchrzrhmul  24223  dchrmulcl  24226  dchrn0  24227  dchrinvcl  24230  dchrfi  24232  dchrsum2  24245  sum2dchr  24251  lgsqrlem1  24318  lgsqrlem2  24319  lgsqrlem3  24320  lgsqrlem4  24321  lgseisenlem3  24328  lgseisenlem4  24329  dchrisum0flblem1  24395  psgnid  28659  mdetpmtr1  28698  iistmd  28757  xrge0iifmhm  28794  xrge0pluscn  28795  pl1cn  28810  hbtlem4  36030  subrgacs  36111  cntzsdrg  36113  idomrootle  36114  isdomn3  36126  mon1psubm  36128  deg1mhm  36129  amgm2d  36694  amgm3d  36695  amgm4d  36696  isringrng  40154  rngcl  40156  isrnghmmul  40166  rnghmf1o  40176  idrnghm  40181  c0rhm  40185  c0rnghm  40186  lidlmmgm  40198  lidlmsgrp  40199  2zrngmmgm  40219  2zrngmsgrp  40220  2zrngnring  40225  cznrng  40230  cznnring  40231  mgpsumunsn  40416  mgpsumz  40417  mgpsumn  40418  invginvrid  40425  ply1vr1smo  40446  ply1mulgsumlem4  40454  ply1mulgsum  40455
  Copyright terms: Public domain W3C validator