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

Theorem mgpbas 18693
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 . . 3 𝑀 = (mulGrp‘𝑅)
3 df-base 16070 . . 3 Base = Slot 1
4 1nn 11312 . . 3 1 ∈ ℕ
5 1ne2 11503 . . 3 1 ≠ 2
62, 3, 4, 5mgplem 18692 . 2 (Base‘𝑅) = (Base‘𝑀)
71, 6eqtri 2828 1 𝐵 = (Base‘𝑀)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  cfv 6097  1c1 10218  Basecbs 16064  mulGrpcmgp 18687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-nn 11302  df-2 11360  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-plusg 16162  df-mgp 18688
This theorem is referenced by:  mgptopn  18696  mgpress  18698  dfur2  18702  srgcl  18710  srgass  18711  srgideu  18712  srgidcl  18716  srgidmlem  18718  issrgid  18721  srg1zr  18727  srgpcomp  18730  srgpcompp  18731  srgpcomppsc  18732  srgbinomlem1  18738  srgbinomlem4  18741  srgbinomlem  18742  srgbinom  18743  csrgbinom  18744  ringcl  18759  crngcom  18760  iscrng2  18761  ringass  18762  ringideu  18763  ringidcl  18766  ringidmlem  18768  isringid  18771  ringidss  18775  ringpropd  18780  crngpropd  18781  isringd  18783  iscrngd  18784  ring1  18800  gsummgp0  18806  prdsmgp  18808  oppr1  18832  unitgrpbas  18864  unitsubm  18868  rngidpropd  18893  dfrhm2  18917  rhmmul  18927  isrhm2d  18928  idrhm  18931  rhmf1o  18932  pwsco1rhm  18938  pwsco2rhm  18939  isdrng2  18957  drngmcl  18960  drngid2  18963  isdrngd  18972  subrgsubm  18993  issubrg3  19008  cntzsubr  19012  pwsdiagrhm  19013  rhmpropd  19015  rlmscaf  19413  sraassa  19530  assamulgscmlem1  19553  assamulgscmlem2  19554  psrcrng  19618  mplcoe3  19671  mplcoe5lem  19672  mplcoe5  19673  mplbas2  19675  evlslem6  19717  evlslem3  19718  evlslem1  19719  mpfind  19740  ply1moncl  19845  coe1tm  19847  coe1pwmul  19853  ply1scltm  19855  ply1coefsupp  19869  ply1coe  19870  gsummoncoe1  19878  lply1binomsc  19881  evls1gsummul  19894  evls1varpw  19895  evl1expd  19913  evl1gsummul  19928  evl1scvarpw  19931  evl1scvarpwval  19932  evl1gsummon  19933  xrsmcmn  19973  cnfldexp  19983  cnmsubglem  20013  expmhm  20019  nn0srg  20020  rge0srg  20021  expghm  20048  cnmsgnbas  20127  ringvcl  20411  mamuvs2  20419  matgsumcl  20474  madetsmelbas  20478  madetsmelbas2  20479  mat1mhm  20498  scmatmhm  20548  mdetleib2  20602  mdetf  20609  m1detdiag  20611  mdetdiaglem  20612  mdetdiag  20613  mdetdiagid  20614  mdetrlin  20616  mdetrsca  20617  mdetralt  20622  mdetunilem7  20632  mdetunilem8  20633  mdetuni0  20635  m2detleiblem2  20642  m2detleiblem3  20643  m2detleiblem4  20644  smadiadetlem4  20684  mat2pmatmhm  20748  pmatcollpwscmatlem1  20804  mply1topmatcllem  20818  mply1topmatcl  20820  pm2mpghm  20831  pm2mpmhm  20835  monmat2matmon  20839  pm2mp  20840  chpscmat  20857  chpscmatgsumbin  20859  chpscmatgsummon  20860  chp0mat  20861  chpidmat  20862  chfacfscmulcl  20872  chfacfscmul0  20873  chfacfscmulgsum  20875  chfacfpmmulcl  20876  chfacfpmmul0  20877  chfacfpmmulgsum  20879  chfacfpmmulgsum2  20880  cayhamlem1  20881  cpmadugsumlemB  20889  cpmadugsumlemC  20890  cpmadugsumlemF  20891  cayhamlem2  20899  cayhamlem4  20903  nrgtrg  22704  deg1pw  24093  ply1remlem  24135  fta1blem  24141  plypf1  24181  efabl  24510  efsubm  24511  amgm  24930  wilthlem2  25008  wilthlem3  25009  dchrelbas2  25175  dchrelbas3  25176  dchrzrhmul  25184  dchrmulcl  25187  dchrn0  25188  dchrinvcl  25191  dchrfi  25193  dchrsum2  25206  sum2dchr  25212  lgsqrlem1  25284  lgsqrlem2  25285  lgsqrlem3  25286  lgsqrlem4  25287  lgseisenlem3  25315  lgseisenlem4  25316  dchrisum0flblem1  25410  psgnid  30171  mdetpmtr1  30213  iistmd  30272  xrge0iifmhm  30309  xrge0pluscn  30310  pl1cn  30325  hbtlem4  38194  subrgacs  38268  cntzsdrg  38270  idomrootle  38271  isdomn3  38280  mon1psubm  38282  deg1mhm  38283  amgm2d  38998  amgm3d  38999  amgm4d  39000  isringrng  42446  rngcl  42448  isrnghmmul  42458  rnghmf1o  42468  idrnghm  42473  c0rhm  42477  c0rnghm  42478  lidlmmgm  42490  lidlmsgrp  42491  2zrngmmgm  42511  2zrngmsgrp  42512  2zrngnring  42517  cznrng  42520  cznnring  42521  mgpsumunsn  42705  mgpsumz  42706  mgpsumn  42707  invginvrid  42713  ply1vr1smo  42734  ply1mulgsumlem4  42742  ply1mulgsum  42743  amgmlemALT  43117  amgmw2d  43118
  Copyright terms: Public domain W3C validator