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

Theorem mgpbas 19176
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 16479 . . 3 Base = Slot 1
4 1nn 11638 . . 3 1 ∈ ℕ
5 1ne2 11834 . . 3 1 ≠ 2
62, 3, 4, 5mgplem 19175 . 2 (Base‘𝑅) = (Base‘𝑀)
71, 6eqtri 2844 1 𝐵 = (Base‘𝑀)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  cfv 6349  1c1 10527  Basecbs 16473  mulGrpcmgp 19170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-2 11689  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-plusg 16568  df-mgp 19171
This theorem is referenced by:  mgptopn  19179  mgpress  19181  dfur2  19185  srgcl  19193  srgass  19194  srgideu  19195  srgidcl  19199  srgidmlem  19201  issrgid  19204  srg1zr  19210  srgpcomp  19213  srgpcompp  19214  srgpcomppsc  19215  srgbinomlem1  19221  srgbinomlem4  19224  srgbinomlem  19225  srgbinom  19226  csrgbinom  19227  ringcl  19242  crngcom  19243  iscrng2  19244  ringass  19245  ringideu  19246  ringidcl  19249  ringidmlem  19251  isringid  19254  ringidss  19258  ringpropd  19263  crngpropd  19264  isringd  19266  iscrngd  19267  ring1  19283  gsummgp0  19289  prdsmgp  19291  oppr1  19315  unitgrpbas  19347  unitsubm  19351  rngidpropd  19376  dfrhm2  19400  rhmmul  19410  isrhm2d  19411  idrhm  19414  rhmf1o  19415  pwsco1rhm  19421  pwsco2rhm  19422  isdrng2  19443  drngmcl  19446  drngid2  19449  isdrngd  19458  subrgsubm  19479  issubrg3  19494  cntzsubr  19499  pwsdiagrhm  19500  rhmpropd  19502  subrgacs  19510  cntzsdrg  19512  subdrgint  19513  primefld  19515  rlmscaf  19911  sraassa  20029  assamulgscmlem1  20058  assamulgscmlem2  20059  psrcrng  20123  mplcoe3  20177  mplcoe5lem  20178  mplcoe5  20179  mplbas2  20181  evlslem3  20223  evlslem6  20224  evlslem1  20225  evlsgsummul  20235  evlspw  20236  mpfind  20250  ply1moncl  20369  coe1tm  20371  coe1pwmul  20377  ply1scltm  20379  ply1coefsupp  20393  ply1coe  20394  gsummoncoe1  20402  lply1binomsc  20405  evls1gsummul  20418  evls1pw  20419  evl1expd  20438  evl1gsummul  20453  evl1scvarpw  20456  evl1scvarpwval  20457  evl1gsummon  20458  xrsmcmn  20498  cnfldexp  20508  cnmsubglem  20538  expmhm  20544  nn0srg  20545  rge0srg  20546  expghm  20573  cnmsgnbas  20652  ringvcl  20939  mamuvs2  20945  matgsumcl  20999  madetsmelbas  21003  madetsmelbas2  21004  mat1mhm  21023  scmatmhm  21073  mdetleib2  21127  mdetf  21134  m1detdiag  21136  mdetdiaglem  21137  mdetdiag  21138  mdetdiagid  21139  mdetrlin  21141  mdetrsca  21142  mdetralt  21147  mdetunilem7  21157  mdetunilem8  21158  mdetuni0  21160  m2detleiblem2  21167  m2detleiblem3  21168  m2detleiblem4  21169  smadiadetlem4  21208  mat2pmatmhm  21271  pmatcollpwscmatlem1  21327  mply1topmatcllem  21341  mply1topmatcl  21343  pm2mpghm  21354  pm2mpmhm  21358  monmat2matmon  21362  pm2mp  21363  chpscmat  21380  chpscmatgsumbin  21382  chpscmatgsummon  21383  chp0mat  21384  chpidmat  21385  chfacfscmulcl  21395  chfacfscmul0  21396  chfacfscmulgsum  21398  chfacfpmmulcl  21399  chfacfpmmul0  21400  chfacfpmmulgsum  21402  chfacfpmmulgsum2  21403  cayhamlem1  21404  cpmadugsumlemB  21412  cpmadugsumlemC  21413  cpmadugsumlemF  21414  cayhamlem2  21422  cayhamlem4  21426  nrgtrg  23228  deg1pw  24643  ply1remlem  24685  fta1blem  24691  plypf1  24731  efabl  25061  efsubm  25062  amgm  25496  wilthlem2  25574  wilthlem3  25575  dchrelbas2  25741  dchrelbas3  25742  dchrzrhmul  25750  dchrmulcl  25753  dchrn0  25754  dchrinvcl  25757  dchrfi  25759  dchrsum2  25772  sum2dchr  25778  lgsqrlem1  25850  lgsqrlem2  25851  lgsqrlem3  25852  lgsqrlem4  25853  lgseisenlem3  25881  lgseisenlem4  25882  dchrisum0flblem1  26012  cntrcrng  30625  psgnid  30667  cnmsgn0g  30716  altgnsg  30719  freshmansdream  30787  cringm4  30881  mdetpmtr1  30988  iistmd  31045  xrge0iifmhm  31082  xrge0pluscn  31083  pl1cn  31098  hbtlem4  39606  idomrootle  39675  isdomn3  39684  mon1psubm  39686  deg1mhm  39687  amgm2d  40432  amgm3d  40433  amgm4d  40434  isringrng  44050  rngcl  44052  isrnghmmul  44062  rnghmf1o  44072  idrnghm  44077  c0rhm  44081  c0rnghm  44082  lidlmmgm  44094  lidlmsgrp  44095  2zrngmmgm  44115  2zrngmsgrp  44116  2zrngnring  44121  cznrng  44124  cznnring  44125  mgpsumunsn  44307  mgpsumz  44308  mgpsumn  44309  invginvrid  44313  ply1vr1smo  44333  ply1mulgsumlem4  44341  ply1mulgsum  44342  amgmlemALT  44802  amgmw2d  44803
  Copyright terms: Public domain W3C validator