Theorem mgpbas 19244

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 16488	. . 3 ⊢ Base = Slot 1
4		1nn 11648	. . 3 ⊢ 1 ∈ ℕ
5		1ne2 11844	. . 3 ⊢ 1 ≠ 2
6	2, 3, 4, 5	mgplem 19243	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
7	1, 6	eqtri 2844	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1533  ‘cfv 6354  1c1 10537  Basecbs 16482  mulGrpcmgp 19238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  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 3496  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 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7580  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-nn 11638  df-2 11699  df-ndx 16485  df-slot 16486  df-base 16488  df-sets 16489  df-plusg 16577  df-mgp 19239

This theorem is referenced by:  mgptopn  19247  mgpress  19249  dfur2  19253  srgcl  19261  srgass  19262  srgideu  19263  srgidcl  19267  srgidmlem  19269  issrgid  19272  srg1zr  19278  srgpcomp  19281  srgpcompp  19282  srgpcomppsc  19283  srgbinomlem1  19289  srgbinomlem4  19292  srgbinomlem  19293  srgbinom  19294  csrgbinom  19295  ringcl  19310  crngcom  19311  iscrng2  19312  ringass  19313  ringideu  19314  ringidcl  19317  ringidmlem  19319  isringid  19322  ringidss  19326  ringpropd  19331  crngpropd  19332  isringd  19334  iscrngd  19335  ring1  19351  gsummgp0  19357  prdsmgp  19359  oppr1  19383  unitgrpbas  19415  unitsubm  19419  rngidpropd  19444  dfrhm2  19468  rhmmul  19478  isrhm2d  19479  idrhm  19482  rhmf1o  19483  pwsco1rhm  19489  pwsco2rhm  19490  isdrng2  19511  drngmcl  19514  drngid2  19517  isdrngd  19526  subrgsubm  19547  issubrg3  19562  cntzsubr  19567  pwsdiagrhm  19568  rhmpropd  19570  subrgacs  19578  cntzsdrg  19580  subdrgint  19581  primefld  19583  rlmscaf  19980  sraassa  20098  assamulgscmlem1  20127  assamulgscmlem2  20128  psrcrng  20192  mplcoe3  20246  mplcoe5lem  20247  mplcoe5  20248  mplbas2  20250  evlslem3  20292  evlslem6  20293  evlslem1  20294  evlsgsummul  20304  evlspw  20305  mpfind  20319  ply1moncl  20438  coe1tm  20440  coe1pwmul  20446  ply1scltm  20448  ply1coefsupp  20462  ply1coe  20463  gsummoncoe1  20471  lply1binomsc  20474  evls1gsummul  20487  evls1pw  20488  evl1expd  20507  evl1gsummul  20522  evl1scvarpw  20525  evl1scvarpwval  20526  evl1gsummon  20527  xrsmcmn  20567  cnfldexp  20577  cnmsubglem  20607  expmhm  20613  nn0srg  20614  rge0srg  20615  expghm  20642  cnmsgnbas  20721  ringvcl  21008  mamuvs2  21014  matgsumcl  21068  madetsmelbas  21072  madetsmelbas2  21073  mat1mhm  21092  scmatmhm  21142  mdetleib2  21196  mdetf  21203  m1detdiag  21205  mdetdiaglem  21206  mdetdiag  21207  mdetdiagid  21208  mdetrlin  21210  mdetrsca  21211  mdetralt  21216  mdetunilem7  21226  mdetunilem8  21227  mdetuni0  21229  m2detleiblem2  21236  m2detleiblem3  21237  m2detleiblem4  21238  smadiadetlem4  21277  mat2pmatmhm  21340  pmatcollpwscmatlem1  21396  mply1topmatcllem  21410  mply1topmatcl  21412  pm2mpghm  21423  pm2mpmhm  21427  monmat2matmon  21431  pm2mp  21432  chpscmat  21449  chpscmatgsumbin  21451  chpscmatgsummon  21452  chp0mat  21453  chpidmat  21454  chfacfscmulcl  21464  chfacfscmul0  21465  chfacfscmulgsum  21467  chfacfpmmulcl  21468  chfacfpmmul0  21469  chfacfpmmulgsum  21471  chfacfpmmulgsum2  21472  cayhamlem1  21473  cpmadugsumlemB  21481  cpmadugsumlemC  21482  cpmadugsumlemF  21483  cayhamlem2  21491  cayhamlem4  21495  nrgtrg  23298  deg1pw  24713  ply1remlem  24755  fta1blem  24761  plypf1  24801  efabl  25133  efsubm  25134  amgm  25567  wilthlem2  25645  wilthlem3  25646  dchrelbas2  25812  dchrelbas3  25813  dchrzrhmul  25821  dchrmulcl  25824  dchrn0  25825  dchrinvcl  25828  dchrfi  25830  dchrsum2  25843  sum2dchr  25849  lgsqrlem1  25921  lgsqrlem2  25922  lgsqrlem3  25923  lgsqrlem4  25924  lgseisenlem3  25952  lgseisenlem4  25953  dchrisum0flblem1  26083  cntrcrng  30697  psgnid  30739  cnmsgn0g  30788  altgnsg  30791  freshmansdream  30859  elringlsm  30946  ringlsmss  30947  lsmsnpridl  30948  cringm4  30962  mxidlprm  30977  mdetpmtr1  31088  iistmd  31145  xrge0iifmhm  31182  xrge0pluscn  31183  pl1cn  31198  hbtlem4  39724  idomrootle  39793  isdomn3  39802  mon1psubm  39804  deg1mhm  39805  amgm2d  40549  amgm3d  40550  amgm4d  40551  isringrng  44151  rngcl  44153  isrnghmmul  44163  rnghmf1o  44173  idrnghm  44178  c0rhm  44182  c0rnghm  44183  lidlmmgm  44195  lidlmsgrp  44196  2zrngmmgm  44216  2zrngmsgrp  44217  2zrngnring  44222  cznrng  44225  cznnring  44226  mgpsumunsn  44408  mgpsumz  44409  mgpsumn  44410  invginvrid  44414  ply1vr1smo  44434  ply1mulgsumlem4  44442  ply1mulgsum  44443  amgmlemALT  44903  amgmw2d  44904