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

Theorem mgpbas 16585
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 14171 . . 3  |-  Base  = Slot  1
4 1nn 10325 . . 3  |-  1  e.  NN
5 1ne2 10526 . . 3  |-  1  =/=  2
62, 3, 4, 5mgplem 16584 . 2  |-  ( Base `  R )  =  (
Base `  M )
71, 6eqtri 2458 1  |-  B  =  ( Base `  M
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   ` cfv 5413   1c1 9275   Basecbs 14166  mulGrpcmgp 16579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-recs 6824  df-rdg 6858  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-plusg 14243  df-mgp 16580
This theorem is referenced by:  mgptopn  16588  mgpress  16590  dfur2  16594  srgcl  16602  srgass  16603  srgideu  16604  srgidcl  16607  srgidmlem  16609  issrgid  16612  srgpcomp  16619  srgpcompp  16620  srgpcomppsc  16621  srgbinomlem1  16626  srgbinomlem4  16629  srgbinomlem  16630  srgbinom  16631  csrgbinom  16632  rngcl  16646  crngcom  16647  iscrng2  16648  rngass  16649  rngideu  16650  rngidcl  16653  rngidmlem  16655  isrngid  16658  rngidss  16659  rngpropd  16664  crngpropd  16665  isrngd  16667  iscrngd  16668  gsummgp0  16687  prdsmgp  16690  oppr1  16714  unitgrpbas  16746  unitsubm  16750  rngidpropd  16775  dfrhm2  16796  rhmmul  16803  isrhm2d  16804  pwsco1rhm  16808  pwsco2rhm  16809  isdrng2  16820  drngmcl  16823  drngid2  16826  isdrngd  16835  subrgsubm  16856  issubrg3  16871  cntzsubr  16875  pwsdiagrhm  16876  rhmpropd  16878  rlmscaf  17266  sraassa  17373  psrcrng  17462  mplcoe3  17522  mplcoe3OLD  17523  mplcoe2  17524  mplcoe2OLD  17525  mplbas2  17526  mplbas2OLD  17527  evlslem6  17573  evlslem6OLD  17574  evlslem3  17575  evlslem1  17576  mpfind  17597  ply1tmcl  17700  coe1tm  17701  coe1pwmul  17707  ply1scltm  17709  ply1coefsupp  17720  ply1coe  17721  ply1coeOLD  17722  evls1gsummul  17735  evls1varpw  17736  evl1expd  17754  evl1gsummul  17769  evl1scvarpw  17772  evl1scvarpwval  17773  evl1gsummon  17774  xrsmcmn  17814  cnfldexp  17824  cnmsubglem  17850  expmhm  17855  nn0srg  17856  rge0srg  17857  expghm  17898  expghmOLD  17899  cnmsgnbas  17983  rngvcl  18273  mamuvs2  18285  matgsumcl  18320  madetsmelbas  18324  madetsmelbas2  18325  mdetleib2  18374  mdetf  18381  mdet1  18383  mdetrlin  18384  mdetrsca  18385  mdetralt  18389  mdetunilem7  18399  mdetunilem8  18400  mdetuni0  18402  m2detleiblem2  18409  m2detleiblem3  18410  m2detleiblem4  18411  smadiadetlem4  18450  nrgtrg  20245  deg1pwle  21566  deg1pw  21567  ply1remlem  21609  fta1blem  21615  plypf1  21655  amgm  22359  wilthlem2  22382  wilthlem3  22383  dchrelbas2  22551  dchrelbas3  22552  dchrzrhmul  22560  dchrmulcl  22563  dchrn0  22564  dchrinvcl  22567  dchrfi  22569  dchrsum2  22582  sum2dchr  22588  lgsqrlem1  22655  lgsqrlem2  22656  lgsqrlem3  22657  lgsqrlem4  22658  lgseisenlem3  22665  lgseisenlem4  22666  dchrisum0flblem1  22732  iistmd  26284  xrge0iifmhm  26321  xrge0pluscn  26322  pl1cn  26337  hbtlem4  29435  subrgacs  29510  cntzsdrg  29512  idomrootle  29513  isdomn3  29525  mon1psubm  29527  deg1mhm  29528  mgpsumunsn  30710  mgpsumz  30711  mgpsumn  30712  invginvrid  30723  assamulgscmlem1  30759  assamulgscmlem2  30760  ply1vr1smo  30764  ply1moncl  30765  lply1binomsc  30775  pmatcollpw1lem4  30817  pmatcollpw1  30819  pmatcollpw2lem  30820  pmatcollpw2  30821  m1detdiag  30823  mdetdiaglem  30824  mdetdiag  30825  mdetdiagid  30826  rng1  30914
  Copyright terms: Public domain W3C validator