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

Theorem mgpbas 20074
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
StepHypRef Expression
1 mgpbas.2 . 2 𝐵 = (Base‘𝑅)
2 mgpbas.1 . . . 4 𝑀 = (mulGrp‘𝑅)
3 eqid 2728 . . . 4 (.r𝑅) = (.r𝑅)
42, 3mgpval 20071 . . 3 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r𝑅)⟩)
5 baseid 17177 . . 3 Base = Slot (Base‘ndx)
6 basendxnplusgndx 17257 . . 3 (Base‘ndx) ≠ (+g‘ndx)
74, 5, 6setsplusg 19295 . 2 (Base‘𝑅) = (Base‘𝑀)
81, 7eqtri 2756 1 𝐵 = (Base‘𝑀)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  cfv 6543  Basecbs 17174  .rcmulr 17228  mulGrpcmgp 20068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7866  df-2nd 7989  df-frecs 8281  df-wrecs 8312  df-recs 8386  df-rdg 8425  df-er 8719  df-en 8959  df-dom 8960  df-sdom 8961  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-nn 12238  df-2 12300  df-sets 17127  df-slot 17145  df-ndx 17157  df-base 17175  df-plusg 17240  df-mgp 20069
This theorem is referenced by:  mgptopn  20080  mgpress  20083  mgpressOLD  20084  prdsmgp  20085  rngass  20093  rngcl  20098  isrngd  20107  rngpropd  20108  dfur2  20118  srgcl  20127  srgass  20128  srgideu  20129  srgidcl  20133  srgidmlem  20135  issrgid  20138  srg1zr  20149  srgpcomp  20152  srgpcompp  20153  srgpcomppsc  20154  srgbinomlem1  20160  srgbinomlem4  20163  srgbinomlem  20164  srgbinom  20165  csrgbinom  20166  ringcl  20184  crngcom  20185  iscrng2  20186  ringass  20187  ringideu  20188  crngbascntr  20190  ringidcl  20196  ringidmlem  20198  isringid  20201  ringidss  20207  isringrng  20217  ringpropd  20218  crngpropd  20219  isringd  20221  iscrngd  20222  ring1  20240  gsummgp0  20248  pwspjmhmmgpd  20258  pwsexpg  20259  xpsring1d  20263  oppr1  20283  unitgrpbas  20315  unitsubm  20319  rngidpropd  20348  isrnghmmul  20375  rnghmf1o  20385  idrnghm  20391  dfrhm2  20407  rhmmul  20419  isrhm2d  20420  idrhm  20423  rhmf1o  20424  pwsco1rhm  20435  pwsco2rhm  20436  c0rhm  20465  c0rnghm  20466  rhmimasubrnglem  20496  rhmimasubrng  20497  cntzsubrng  20498  subrgsubm  20518  issubrg3  20533  cntzsubr  20539  pwsdiagrhm  20540  rhmpropd  20542  isdrng2  20632  drngmcl  20635  drngid2  20639  isdrngd  20651  isdrngdOLD  20653  subrgacs  20682  cntzsdrg  20684  subdrgint  20685  primefld  20687  rlmscaf  21094  rnglidlmmgm  21134  rnglidlmsgrp  21135  rng2idl1cntr  21189  isdomn3  21242  xrsmcmn  21313  cnfldexp  21326  cnmsubglem  21357  expmhm  21363  nn0srg  21364  rge0srg  21365  expghm  21395  fermltlchr  21453  freshmansdream  21502  cnmsgnbas  21504  sraassab  21795  sraassaOLD  21797  assamulgscmlem1  21826  assamulgscmlem2  21827  psrcrng  21909  mplcoe3  21970  mplcoe5lem  21971  mplcoe5  21972  mplbas2  21974  evlslem3  22020  evlslem6  22021  evlslem1  22022  evlsgsummul  22032  evlspw  22033  mpfind  22047  mhppwdeg  22068  ply1moncl  22184  coe1tm  22186  coe1pwmul  22192  ply1scltm  22194  ply1coefsupp  22210  ply1coe  22211  gsummoncoe1  22221  lply1binomsc  22224  ply1fermltlchr  22225  evls1gsummul  22238  evls1pw  22239  evl1expd  22258  evl1gsummul  22273  evl1scvarpw  22276  evl1scvarpwval  22277  evl1gsummon  22278  ringvcl  22294  mamuvs2  22300  matgsumcl  22356  madetsmelbas  22360  madetsmelbas2  22361  mat1mhm  22380  scmatmhm  22430  mdetleib2  22484  mdetf  22491  m1detdiag  22493  mdetdiaglem  22494  mdetdiag  22495  mdetdiagid  22496  mdetrlin  22498  mdetrsca  22499  mdetralt  22504  mdetunilem7  22514  mdetunilem8  22515  mdetuni0  22517  m2detleiblem2  22524  m2detleiblem3  22525  m2detleiblem4  22526  smadiadetlem4  22565  mat2pmatmhm  22629  pmatcollpwscmatlem1  22685  mply1topmatcllem  22699  mply1topmatcl  22701  pm2mpghm  22712  pm2mpmhm  22716  monmat2matmon  22720  pm2mp  22721  chpscmat  22738  chpscmatgsumbin  22740  chpscmatgsummon  22741  chp0mat  22742  chpidmat  22743  chfacfscmulcl  22753  chfacfscmul0  22754  chfacfscmulgsum  22756  chfacfpmmulcl  22757  chfacfpmmul0  22758  chfacfpmmulgsum  22760  chfacfpmmulgsum2  22761  cayhamlem1  22762  cpmadugsumlemB  22770  cpmadugsumlemC  22771  cpmadugsumlemF  22772  cayhamlem2  22780  cayhamlem4  22784  nrgtrg  24601  deg1pw  26050  ply1remlem  26093  fta1blem  26099  idomrootle  26101  plypf1  26140  efabl  26478  efsubm  26479  amgm  26917  wilthlem2  26995  wilthlem3  26996  dchrelbas2  27164  dchrelbas3  27165  dchrzrhmul  27173  dchrmulcl  27176  dchrn0  27177  dchrinvcl  27180  dchrfi  27182  dchrsum2  27195  sum2dchr  27201  lgsqrlem1  27273  lgsqrlem2  27274  lgsqrlem3  27275  lgsqrlem4  27276  lgseisenlem3  27304  lgseisenlem4  27305  dchrisum0flblem1  27435  cntrcrng  32771  psgnid  32813  cnmsgn0g  32862  altgnsg  32865  urpropd  32934  frobrhm  32936  rrgsubm  32948  erlbr2d  32973  erler  32974  rlocaddval  32977  rlocmulval  32978  rloccring  32979  rloc0g  32980  rloc1r  32981  rlocf1  32982  zringfrac  32991  znfermltl  33073  elringlsm  33097  ringlsmss  33099  lsmsnpridl  33102  cringm4  33157  mxidlprm  33178  evls1fpws  33241  gsummoncoe1fzo  33259  ply1degltdimlem  33311  ply1degltdim  33312  evls1fldgencl  33349  mdetpmtr1  33419  iistmd  33498  xrge0iifmhm  33535  xrge0pluscn  33536  pl1cn  33551  aks6d1c1p2  41575  aks6d1c1p3  41576  aks6d1c1p4  41577  aks6d1c1p5  41578  aks6d1c1p7  41579  aks6d1c1p6  41580  aks6d1c1p8  41581  aks6d1c1  41582  evl1gprodd  41583  aks6d1c2lem4  41593  idomnnzpownz  41598  idomnnzgmulnz  41599  ringexp0nn  41600  aks6d1c5lem0  41601  aks6d1c5lem3  41603  aks6d1c5lem2  41604  aks6d1c5  41605  deg1gprod  41607  deg1pow  41608  aks6d1c6lem1  41637  aks6d1c6lem2  41638  aks6d1c6lem3  41639  pwsgprod  41765  evlsvvvallem  41785  evlsvvval  41787  evlsexpval  41791  selvvvval  41809  evlselv  41811  mhphf  41821  hbtlem4  42541  mon1psubm  42618  deg1mhm  42619  amgm2d  43619  amgm3d  43620  amgm4d  43621  2zrngmmgm  47305  2zrngmsgrp  47306  2zrngnring  47311  cznrng  47314  cznnring  47315  mgpsumunsn  47416  mgpsumz  47417  mgpsumn  47418  invginvrid  47422  ply1vr1smo  47441  ply1mulgsumlem4  47448  ply1mulgsum  47449  amgmlemALT  48227  amgmw2d  48228
  Copyright terms: Public domain W3C validator