Theorem mgpbas 19510

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

Step	Hyp	Ref	Expression
1		mgpbas.2	. 2 ⊢ 𝐵 = (Base‘𝑅)
2		mgpbas.1	. . 3 ⊢ 𝑀 = (mulGrp‘𝑅)
3		df-base 16761	. . 3 ⊢ Base = Slot 1
4		1nn 11841	. . 3 ⊢ 1 ∈ ℕ
5		1ne2 12038	. . 3 ⊢ 1 ≠ 2
6	2, 3, 4, 5	mgplem 19509	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
7	1, 6	eqtri 2765	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1543  ‘cfv 6380  1c1 10730  Basecbs 16760  mulGrpcmgp 19504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-2 11893  df-sets 16717  df-slot 16735  df-ndx 16745  df-base 16761  df-plusg 16815  df-mgp 19505

This theorem is referenced by:  mgptopn  19513  mgpress  19515  dfur2  19519  srgcl  19527  srgass  19528  srgideu  19529  srgidcl  19533  srgidmlem  19535  issrgid  19538  srg1zr  19544  srgpcomp  19547  srgpcompp  19548  srgpcomppsc  19549  srgbinomlem1  19555  srgbinomlem4  19558  srgbinomlem  19559  srgbinom  19560  csrgbinom  19561  ringcl  19579  crngcom  19580  iscrng2  19581  ringass  19582  ringideu  19583  ringidcl  19586  ringidmlem  19588  isringid  19591  ringidss  19595  ringpropd  19600  crngpropd  19601  isringd  19603  iscrngd  19604  ring1  19620  gsummgp0  19626  prdsmgp  19628  oppr1  19652  unitgrpbas  19684  unitsubm  19688  rngidpropd  19713  dfrhm2  19737  rhmmul  19747  isrhm2d  19748  idrhm  19751  rhmf1o  19752  pwsco1rhm  19758  pwsco2rhm  19759  isdrng2  19777  drngmcl  19780  drngid2  19783  isdrngd  19792  subrgsubm  19813  issubrg3  19828  cntzsubr  19833  pwsdiagrhm  19834  rhmpropd  19836  subrgacs  19844  cntzsdrg  19846  subdrgint  19847  primefld  19849  rlmscaf  20246  xrsmcmn  20386  cnfldexp  20396  cnmsubglem  20426  expmhm  20432  nn0srg  20433  rge0srg  20434  expghm  20462  cnmsgnbas  20540  sraassa  20829  assamulgscmlem1  20859  assamulgscmlem2  20860  psrcrng  20938  mplcoe3  20995  mplcoe5lem  20996  mplcoe5  20997  mplbas2  20999  evlslem3  21040  evlslem6  21041  evlslem1  21042  evlsgsummul  21052  evlspw  21053  mpfind  21067  mhppwdeg  21090  ply1moncl  21192  coe1tm  21194  coe1pwmul  21200  ply1scltm  21202  ply1coefsupp  21216  ply1coe  21217  gsummoncoe1  21225  lply1binomsc  21228  evls1gsummul  21241  evls1pw  21242  evl1expd  21261  evl1gsummul  21276  evl1scvarpw  21279  evl1scvarpwval  21280  evl1gsummon  21281  ringvcl  21297  mamuvs2  21303  matgsumcl  21357  madetsmelbas  21361  madetsmelbas2  21362  mat1mhm  21381  scmatmhm  21431  mdetleib2  21485  mdetf  21492  m1detdiag  21494  mdetdiaglem  21495  mdetdiag  21496  mdetdiagid  21497  mdetrlin  21499  mdetrsca  21500  mdetralt  21505  mdetunilem7  21515  mdetunilem8  21516  mdetuni0  21518  m2detleiblem2  21525  m2detleiblem3  21526  m2detleiblem4  21527  smadiadetlem4  21566  mat2pmatmhm  21630  pmatcollpwscmatlem1  21686  mply1topmatcllem  21700  mply1topmatcl  21702  pm2mpghm  21713  pm2mpmhm  21717  monmat2matmon  21721  pm2mp  21722  chpscmat  21739  chpscmatgsumbin  21741  chpscmatgsummon  21742  chp0mat  21743  chpidmat  21744  chfacfscmulcl  21754  chfacfscmul0  21755  chfacfscmulgsum  21757  chfacfpmmulcl  21758  chfacfpmmul0  21759  chfacfpmmulgsum  21761  chfacfpmmulgsum2  21762  cayhamlem1  21763  cpmadugsumlemB  21771  cpmadugsumlemC  21772  cpmadugsumlemF  21773  cayhamlem2  21781  cayhamlem4  21785  nrgtrg  23588  deg1pw  25018  ply1remlem  25060  fta1blem  25066  plypf1  25106  efabl  25439  efsubm  25440  amgm  25873  wilthlem2  25951  wilthlem3  25952  dchrelbas2  26118  dchrelbas3  26119  dchrzrhmul  26127  dchrmulcl  26130  dchrn0  26131  dchrinvcl  26134  dchrfi  26136  dchrsum2  26149  sum2dchr  26155  lgsqrlem1  26227  lgsqrlem2  26228  lgsqrlem3  26229  lgsqrlem4  26230  lgseisenlem3  26258  lgseisenlem4  26259  dchrisum0flblem1  26389  cntrcrng  31041  psgnid  31083  cnmsgn0g  31132  altgnsg  31135  freshmansdream  31203  frobrhm  31204  znfermltl  31276  elringlsm  31295  ringlsmss  31297  lsmsnpridl  31300  cringm4  31336  mxidlprm  31354  ply1fermltl  31384  mdetpmtr1  31487  iistmd  31566  xrge0iifmhm  31603  xrge0pluscn  31604  pl1cn  31619  pwspjmhmmgpd  39979  pwsexpg  39980  pwsgprod  39981  evlsbagval  39985  evlsexpval  39986  mhphf  39995  hbtlem4  40654  idomrootle  40723  isdomn3  40732  mon1psubm  40734  deg1mhm  40735  amgm2d  41487  amgm3d  41488  amgm4d  41489  isringrng  45112  rngcl  45114  isrnghmmul  45124  rnghmf1o  45134  idrnghm  45139  c0rhm  45143  c0rnghm  45144  lidlmmgm  45156  lidlmsgrp  45157  2zrngmmgm  45177  2zrngmsgrp  45178  2zrngnring  45183  cznrng  45186  cznnring  45187  mgpsumunsn  45370  mgpsumz  45371  mgpsumn  45372  invginvrid  45376  ply1vr1smo  45395  ply1mulgsumlem4  45403  ply1mulgsum  45404  amgmlemALT  46178  amgmw2d  46179