Theorem mgpbas 18940

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 16323	. . 3 ⊢ Base = Slot 1
4		1nn 11502	. . 3 ⊢ 1 ∈ ℕ
5		1ne2 11698	. . 3 ⊢ 1 ≠ 2
6	2, 3, 4, 5	mgplem 18939	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
7	1, 6	eqtri 2819	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1522  ‘cfv 6230  1c1 10389  Basecbs 16317  mulGrpcmgp 18934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-cnex 10444  ax-resscn 10445  ax-1cn 10446  ax-icn 10447  ax-addcl 10448  ax-addrcl 10449  ax-mulcl 10450  ax-mulrcl 10451  ax-mulcom 10452  ax-addass 10453  ax-mulass 10454  ax-distr 10455  ax-i2m1 10456  ax-1ne0 10457  ax-1rid 10458  ax-rnegex 10459  ax-rrecex 10460  ax-cnre 10461  ax-pre-lttri 10462  ax-pre-lttrn 10463  ax-pre-ltadd 10464  ax-pre-mulgt0 10465

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-pred 6028  df-ord 6074  df-on 6075  df-lim 6076  df-suc 6077  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-riota 6982  df-ov 7024  df-oprab 7025  df-mpo 7026  df-om 7442  df-wrecs 7803  df-recs 7865  df-rdg 7903  df-er 8144  df-en 8363  df-dom 8364  df-sdom 8365  df-pnf 10528  df-mnf 10529  df-xr 10530  df-ltxr 10531  df-le 10532  df-sub 10724  df-neg 10725  df-nn 11492  df-2 11553  df-ndx 16320  df-slot 16321  df-base 16323  df-sets 16324  df-plusg 16412  df-mgp 18935

This theorem is referenced by:  mgptopn  18943  mgpress  18945  dfur2  18949  srgcl  18957  srgass  18958  srgideu  18959  srgidcl  18963  srgidmlem  18965  issrgid  18968  srg1zr  18974  srgpcomp  18977  srgpcompp  18978  srgpcomppsc  18979  srgbinomlem1  18985  srgbinomlem4  18988  srgbinomlem  18989  srgbinom  18990  csrgbinom  18991  ringcl  19006  crngcom  19007  iscrng2  19008  ringass  19009  ringideu  19010  ringidcl  19013  ringidmlem  19015  isringid  19018  ringidss  19022  ringpropd  19027  crngpropd  19028  isringd  19030  iscrngd  19031  ring1  19047  gsummgp0  19053  prdsmgp  19055  oppr1  19079  unitgrpbas  19111  unitsubm  19115  rngidpropd  19140  dfrhm2  19164  rhmmul  19174  isrhm2d  19175  idrhm  19178  rhmf1o  19179  pwsco1rhm  19185  pwsco2rhm  19186  isdrng2  19207  drngmcl  19210  drngid2  19213  isdrngd  19222  subrgsubm  19243  issubrg3  19258  cntzsubr  19263  pwsdiagrhm  19264  rhmpropd  19266  subrgacs  19274  cntzsdrg  19276  subdrgint  19277  primefld  19279  rlmscaf  19675  sraassa  19792  assamulgscmlem1  19821  assamulgscmlem2  19822  psrcrng  19886  mplcoe3  19939  mplcoe5lem  19940  mplcoe5  19941  mplbas2  19943  evlslem6  19985  evlslem3  19986  evlslem1  19987  mpfind  20008  ply1moncl  20127  coe1tm  20129  coe1pwmul  20135  ply1scltm  20137  ply1coefsupp  20151  ply1coe  20152  gsummoncoe1  20160  lply1binomsc  20163  evls1gsummul  20176  evls1varpw  20177  evl1expd  20195  evl1gsummul  20210  evl1scvarpw  20213  evl1scvarpwval  20214  evl1gsummon  20215  xrsmcmn  20255  cnfldexp  20265  cnmsubglem  20295  expmhm  20301  nn0srg  20302  rge0srg  20303  expghm  20330  cnmsgnbas  20409  ringvcl  20696  mamuvs2  20704  matgsumcl  20758  madetsmelbas  20762  madetsmelbas2  20763  mat1mhm  20782  scmatmhm  20832  mdetleib2  20886  mdetf  20893  m1detdiag  20895  mdetdiaglem  20896  mdetdiag  20897  mdetdiagid  20898  mdetrlin  20900  mdetrsca  20901  mdetralt  20906  mdetunilem7  20916  mdetunilem8  20917  mdetuni0  20919  m2detleiblem2  20926  m2detleiblem3  20927  m2detleiblem4  20928  smadiadetlem4  20967  mat2pmatmhm  21030  pmatcollpwscmatlem1  21086  mply1topmatcllem  21100  mply1topmatcl  21102  pm2mpghm  21113  pm2mpmhm  21117  monmat2matmon  21121  pm2mp  21122  chpscmat  21139  chpscmatgsumbin  21141  chpscmatgsummon  21142  chp0mat  21143  chpidmat  21144  chfacfscmulcl  21154  chfacfscmul0  21155  chfacfscmulgsum  21157  chfacfpmmulcl  21158  chfacfpmmul0  21159  chfacfpmmulgsum  21161  chfacfpmmulgsum2  21162  cayhamlem1  21163  cpmadugsumlemB  21171  cpmadugsumlemC  21172  cpmadugsumlemF  21173  cayhamlem2  21181  cayhamlem4  21185  nrgtrg  22987  deg1pw  24402  ply1remlem  24444  fta1blem  24450  plypf1  24490  efabl  24820  efsubm  24821  amgm  25255  wilthlem2  25333  wilthlem3  25334  dchrelbas2  25500  dchrelbas3  25501  dchrzrhmul  25509  dchrmulcl  25512  dchrn0  25513  dchrinvcl  25516  dchrfi  25518  dchrsum2  25531  sum2dchr  25537  lgsqrlem1  25609  lgsqrlem2  25610  lgsqrlem3  25611  lgsqrlem4  25612  lgseisenlem3  25640  lgseisenlem4  25641  dchrisum0flblem1  25771  cnmsgn0g  30430  psgnid  30432  altgnsg  30434  cntrcrng  30515  freshmansdream  30518  mdetpmtr1  30708  iistmd  30767  xrge0iifmhm  30804  xrge0pluscn  30805  pl1cn  30820  hbtlem4  39237  idomrootle  39306  isdomn3  39315  mon1psubm  39317  deg1mhm  39318  amgm2d  40063  amgm3d  40064  amgm4d  40065  isringrng  43657  rngcl  43659  isrnghmmul  43669  rnghmf1o  43679  idrnghm  43684  c0rhm  43688  c0rnghm  43689  lidlmmgm  43701  lidlmsgrp  43702  2zrngmmgm  43722  2zrngmsgrp  43723  2zrngnring  43728  cznrng  43731  cznnring  43732  mgpsumunsn  43914  mgpsumz  43915  mgpsumn  43916  invginvrid  43922  ply1vr1smo  43942  ply1mulgsumlem4  43950  ply1mulgsum  43951  amgmlemALT  44411  amgmw2d  44412