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

Theorem mgpbas 17716
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 15113 . . 3  |-  Base  = Slot  1
4 1nn 10620 . . 3  |-  1  e.  NN
5 1ne2 10822 . . 3  |-  1  =/=  2
62, 3, 4, 5mgplem 17715 . 2  |-  ( Base `  R )  =  (
Base `  M )
71, 6eqtri 2451 1  |-  B  =  ( Base `  M
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   ` cfv 5597   1c1 9540   Basecbs 15108  mulGrpcmgp 17710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-ndx 15111  df-slot 15112  df-base 15113  df-sets 15114  df-plusg 15190  df-mgp 17711
This theorem is referenced by:  mgptopn  17719  mgpress  17721  dfur2  17725  srgcl  17733  srgass  17734  srgideu  17735  srgidcl  17738  srgidmlem  17740  issrgid  17743  srg1zr  17749  srgpcomp  17752  srgpcompp  17753  srgpcomppsc  17754  srgbinomlem1  17760  srgbinomlem4  17763  srgbinomlem  17764  srgbinom  17765  csrgbinom  17766  ringcl  17781  crngcom  17782  iscrng2  17783  ringass  17784  ringideu  17785  ringidcl  17788  ringidmlem  17790  isringid  17793  ringidss  17794  ringpropd  17799  crngpropd  17800  isringd  17802  iscrngd  17803  ring1  17817  gsummgp0  17823  prdsmgp  17825  oppr1  17849  unitgrpbas  17881  unitsubm  17885  rngidpropd  17910  dfrhm2  17932  rhmmul  17942  isrhm2d  17943  idrhm  17946  rhmf1o  17947  pwsco1rhm  17953  pwsco2rhm  17954  isdrng2  17972  drngmcl  17975  drngid2  17978  isdrngd  17987  subrgsubm  18008  issubrg3  18023  cntzsubr  18027  pwsdiagrhm  18028  rhmpropd  18030  rlmscaf  18418  sraassa  18536  assamulgscmlem1  18559  assamulgscmlem2  18560  psrcrng  18624  mplcoe3  18677  mplcoe5lem  18678  mplcoe5  18679  mplbas2  18681  evlslem6  18723  evlslem3  18724  evlslem1  18725  mpfind  18746  ply1moncl  18851  coe1tm  18853  coe1pwmul  18859  ply1scltm  18861  ply1coefsupp  18875  ply1coe  18876  ply1coeOLD  18877  gsummoncoe1  18885  lply1binomsc  18888  evls1gsummul  18901  evls1varpw  18902  evl1expd  18920  evl1gsummul  18935  evl1scvarpw  18938  evl1scvarpwval  18939  evl1gsummon  18940  xrsmcmn  18978  cnfldexp  18988  cnmsubglem  19017  expmhm  19022  nn0srg  19023  rge0srg  19024  expghm  19053  cnmsgnbas  19132  ringvcl  19409  mamuvs2  19417  matgsumcl  19471  madetsmelbas  19475  madetsmelbas2  19476  mat1mhm  19495  scmatmhm  19545  mdetleib2  19599  mdetf  19606  m1detdiag  19608  mdetdiaglem  19609  mdetdiag  19610  mdetdiagid  19611  mdetrlin  19613  mdetrsca  19614  mdetralt  19619  mdetunilem7  19629  mdetunilem8  19630  mdetuni0  19632  m2detleiblem2  19639  m2detleiblem3  19640  m2detleiblem4  19641  smadiadetlem4  19680  mat2pmatmhm  19743  pmatcollpwscmatlem1  19799  mply1topmatcllem  19813  mply1topmatcl  19815  pm2mpghm  19826  pm2mpmhm  19830  monmat2matmon  19834  pm2mp  19835  chpscmat  19852  chpscmatgsumbin  19854  chpscmatgsummon  19855  chp0mat  19856  chpidmat  19857  chfacfscmulcl  19867  chfacfscmul0  19868  chfacfscmulgsum  19870  chfacfpmmulcl  19871  chfacfpmmul0  19872  chfacfpmmulgsum  19874  chfacfpmmulgsum2  19875  cayhamlem1  19876  cpmadugsumlemB  19884  cpmadugsumlemC  19885  cpmadugsumlemF  19886  cayhamlem2  19894  cayhamlem4  19898  nrgtrg  21678  deg1pw  23055  ply1remlem  23099  fta1blem  23105  plypf1  23152  efabl  23485  efsubm  23486  amgm  23902  wilthlem2  23980  wilthlem3  23981  dchrelbas2  24151  dchrelbas3  24152  dchrzrhmul  24160  dchrmulcl  24163  dchrn0  24164  dchrinvcl  24167  dchrfi  24169  dchrsum2  24182  sum2dchr  24188  lgsqrlem1  24255  lgsqrlem2  24256  lgsqrlem3  24257  lgsqrlem4  24258  lgseisenlem3  24265  lgseisenlem4  24266  dchrisum0flblem1  24332  psgnid  28605  mdetpmtr1  28644  iistmd  28703  xrge0iifmhm  28740  xrge0pluscn  28741  pl1cn  28756  hbtlem4  35904  subrgacs  35985  cntzsdrg  35987  idomrootle  35988  isdomn3  36000  mon1psubm  36002  deg1mhm  36003  amgm2d  36507  amgm3d  36508  amgm4d  36509  isringrng  39152  rngcl  39154  isrnghmmul  39164  rnghmf1o  39174  idrnghm  39179  c0rhm  39183  c0rnghm  39184  lidlmmgm  39196  lidlmsgrp  39197  2zrngmmgm  39217  2zrngmsgrp  39218  2zrngnring  39223  cznrng  39228  cznnring  39229  mgpsumunsn  39416  mgpsumz  39417  mgpsumn  39418  invginvrid  39425  ply1vr1smo  39446  ply1mulgsumlem4  39454  ply1mulgsum  39455
  Copyright terms: Public domain W3C validator