Theorem mgpbas 20067

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	. . . 4 ⊢ 𝑀 = (mulGrp‘𝑅)
3		eqid 2733	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20065	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17127	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17195	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19266	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2756	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1541  ‘cfv 6488  Basecbs 17124  ._rcmulr 17166  mulGrpcmgp 20062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-cnex 11071  ax-resscn 11072  ax-1cn 11073  ax-icn 11074  ax-addcl 11075  ax-addrcl 11076  ax-mulcl 11077  ax-mulrcl 11078  ax-mulcom 11079  ax-addass 11080  ax-mulass 11081  ax-distr 11082  ax-i2m1 11083  ax-1ne0 11084  ax-1rid 11085  ax-rnegex 11086  ax-rrecex 11087  ax-cnre 11088  ax-pre-lttri 11089  ax-pre-lttrn 11090  ax-pre-ltadd 11091  ax-pre-mulgt0 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7311  df-ov 7357  df-oprab 7358  df-mpo 7359  df-om 7805  df-2nd 7930  df-frecs 8219  df-wrecs 8250  df-recs 8299  df-rdg 8337  df-er 8630  df-en 8878  df-dom 8879  df-sdom 8880  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160  df-le 11161  df-sub 11355  df-neg 11356  df-nn 12135  df-2 12197  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17125  df-plusg 17178  df-mgp 20063

This theorem is referenced by:  mgptopn  20070  mgpress  20072  prdsmgp  20073  rngass  20081  rngcl  20086  isrngd  20095  rngpropd  20096  dfur2  20106  srgcl  20115  srgass  20116  srgideu  20117  srgidcl  20121  srgidmlem  20123  issrgid  20126  srg1zr  20137  srgpcomp  20140  srgpcompp  20141  srgpcomppsc  20142  srgbinomlem1  20148  srgbinomlem4  20151  srgbinomlem  20152  srgbinom  20153  csrgbinom  20154  ringcl  20172  crngcom  20173  iscrng2  20174  ringass  20175  ringideu  20176  crngbascntr  20178  ringidcl  20187  ringidmlem  20190  isringid  20193  ringidss  20199  isringrng  20209  ringpropd  20210  crngpropd  20211  isringd  20213  iscrngd  20214  ring1  20232  gsummgp0  20240  pwspjmhmmgpd  20250  pwsexpg  20251  xpsring1d  20255  oppr1  20272  unitgrpbas  20304  unitsubm  20308  rngidpropd  20337  isrnghmmul  20364  rnghmf1o  20374  idrnghm  20380  dfrhm2  20396  rhmmul  20407  isrhm2d  20408  idrhm  20411  rhmf1o  20412  pwsco1rhm  20421  pwsco2rhm  20422  c0rhm  20453  c0rnghm  20454  rhmimasubrnglem  20484  rhmimasubrng  20485  cntzsubrng  20486  subrgsubm  20504  issubrg3  20519  cntzsubr  20525  pwsdiagrhm  20526  rhmpropd  20528  isdomn3  20634  isdrng2  20662  drngmclOLD  20670  drngid2  20671  isdrngd  20684  isdrngdOLD  20686  subrgacs  20719  cntzsdrg  20721  subdrgint  20722  primefld  20724  rlmscaf  21145  rnglidlmmgm  21186  rnglidlmsgrp  21187  rng2idl1cntr  21246  xrsmcmn  21332  cnfldexp  21345  cnmsubglem  21371  expmhm  21377  nn0srg  21378  rge0srg  21379  expghm  21416  fermltlchr  21470  freshmansdream  21515  frobrhm  21516  cnmsgnbas  21519  sraassab  21809  sraassaOLD  21811  assamulgscmlem1  21840  assamulgscmlem2  21841  psrcrng  21912  mplcoe3  21976  mplcoe5lem  21977  mplcoe5  21978  mplbas2  21980  evlslem3  22018  evlslem6  22019  evlslem1  22020  evlsgsummul  22030  evlspw  22031  mpfind  22045  mhppwdeg  22068  psdpw  22088  ply1moncl  22188  coe1tm  22190  coe1pwmul  22196  ply1scltm  22198  ply1idvr1  22212  ply1coefsupp  22215  ply1coe  22216  gsummoncoe1  22226  lply1binomsc  22229  ply1fermltlchr  22230  evls1gsummul  22243  evls1pw  22244  evl1expd  22263  evl1gsummul  22278  evl1scvarpw  22281  evl1scvarpwval  22282  evl1gsummon  22283  evls1fpws  22287  rhmply1mon  22307  ringvcl  22318  mamuvs2  22324  matgsumcl  22378  madetsmelbas  22382  madetsmelbas2  22383  mat1mhm  22402  scmatmhm  22452  mdetleib2  22506  mdetf  22513  m1detdiag  22515  mdetdiaglem  22516  mdetdiag  22517  mdetdiagid  22518  mdetrlin  22520  mdetrsca  22521  mdetralt  22526  mdetunilem7  22536  mdetunilem8  22537  mdetuni0  22539  m2detleiblem2  22546  m2detleiblem3  22547  m2detleiblem4  22548  smadiadetlem4  22587  mat2pmatmhm  22651  pmatcollpwscmatlem1  22707  mply1topmatcllem  22721  mply1topmatcl  22723  pm2mpghm  22734  pm2mpmhm  22738  monmat2matmon  22742  pm2mp  22743  chpscmat  22760  chpscmatgsumbin  22762  chpscmatgsummon  22763  chp0mat  22764  chpidmat  22765  chfacfscmulcl  22775  chfacfscmul0  22776  chfacfscmulgsum  22778  chfacfpmmulcl  22779  chfacfpmmul0  22780  chfacfpmmulgsum  22782  chfacfpmmulgsum2  22783  cayhamlem1  22784  cpmadugsumlemB  22792  cpmadugsumlemC  22793  cpmadugsumlemF  22794  cayhamlem2  22802  cayhamlem4  22806  nrgtrg  24608  deg1pw  26056  ply1remlem  26100  fta1blem  26106  idomrootle  26108  plypf1  26147  efabl  26489  efsubm  26490  amgm  26931  wilthlem2  27009  wilthlem3  27010  dchrelbas2  27178  dchrelbas3  27179  dchrzrhmul  27187  dchrmulcl  27190  dchrn0  27191  dchrinvcl  27194  dchrfi  27196  dchrsum2  27209  sum2dchr  27215  lgsqrlem1  27287  lgsqrlem2  27288  lgsqrlem3  27289  lgsqrlem4  27290  lgseisenlem3  27318  lgseisenlem4  27319  dchrisum0flblem1  27449  zsoring  28335  cntrcrng  33059  psgnid  33075  cnmsgn0g  33124  altgnsg  33127  urpropd  33208  isunit3  33217  elrgspnlem1  33218  elrgspnlem2  33219  elrgspnlem3  33220  elrgspnlem4  33221  elrgspn  33222  elrgspnsubrunlem1  33223  elrgspnsubrunlem2  33224  0ringcring  33228  erlbr2d  33240  erler  33241  rlocaddval  33244  rlocmulval  33245  rloccring  33246  rloc0g  33247  rloc1r  33248  rlocf1  33249  domnprodn0  33251  rrgsubm  33259  znfermltl  33340  unitprodclb  33363  elringlsm  33367  ringlsmss  33369  lsmsnpridl  33372  cringm4  33420  ssdifidlprm  33432  mxidlprm  33444  rprmdvdspow  33507  rprmdvdsprod  33508  1arithidomlem1  33509  1arithidom  33511  1arithufdlem1  33518  1arithufdlem2  33519  1arithufdlem3  33520  1arithufdlem4  33521  dfufd2lem  33523  zringfrac  33528  ressply1evls1  33537  evl1deg1  33548  evl1deg2  33549  evl1deg3  33550  evls1monply1  33551  coe1vr1  33561  deg1vr  33562  gsummoncoe1fzo  33567  srapwov  33624  ply1degltdimlem  33658  ply1degltdim  33659  assarrginv  33672  evls1fldgencl  33706  extdgfialglem1  33728  extdgfialglem2  33729  rtelextdg2lem  33762  2sqr3minply  33816  cos9thpiminplylem6  33823  cos9thpiminply  33824  mdetpmtr1  33859  iistmd  33938  xrge0iifmhm  33975  xrge0pluscn  33976  pl1cn  33991  zrhcntr  34015  aks6d1c1p2  42225  aks6d1c1p3  42226  aks6d1c1p4  42227  aks6d1c1p5  42228  aks6d1c1p7  42229  aks6d1c1p6  42230  aks6d1c1p8  42231  aks6d1c1  42232  evl1gprodd  42233  aks6d1c2lem4  42243  idomnnzpownz  42248  idomnnzgmulnz  42249  ringexp0nn  42250  aks6d1c5lem0  42251  aks6d1c5lem3  42253  aks6d1c5lem2  42254  aks6d1c5  42255  deg1gprod  42256  deg1pow  42257  aks6d1c6lem1  42286  aks6d1c6lem2  42287  aks6d1c6lem3  42288  aks5lem2  42303  aks5lem3a  42305  unitscyglem5  42315  aks5lem7  42316  domnexpgn0cl  42644  abvexp  42653  fidomncyc  42656  pwsgprod  42665  evlsvvvallem  42682  evlsvvval  42684  evlsexpval  42688  selvvvval  42706  evlselv  42708  mhphf  42718  hbtlem4  43246  mon1psubm  43319  deg1mhm  43320  amgm2d  44318  amgm3d  44319  amgm4d  44320  2zrngmmgm  48379  2zrngmsgrp  48380  2zrngnring  48385  cznrng  48388  cznnring  48389  mgpsumunsn  48488  mgpsumz  48489  mgpsumn  48490  invginvrid  48494  ply1vr1smo  48510  ply1mulgsumlem4  48517  ply1mulgsum  48518  elmgpcntrd  49132  amgmlemALT  49931  amgmw2d  49932