Theorem mgpbas 20284

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 2762	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20282	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17310	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17378	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19483	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2785	1 ⊢ 𝐵 = (Base‘𝑀)

This proof depends on syntax axioms:   = wceq 1570  ‘cfv 6537  Basecbs 17307  ._rcmulr 17349  mulGrpcmgp 20279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-nn 12262  df-2 12331  df-sets 17262  df-slot 17280  df-ndx 17292  df-base 17308  df-plusg 17361  df-mgp 20280

This theorem is used by:  mgptopn  20287  mgpress  20289  prdsmgp  20290  elmgplsm  20291  rngass  20300  rngcl  20305  isrngd  20314  rngpropd  20315  rng1zrlem  20322  dfur2  20329  srgcl  20338  srgass  20339  srgideu  20340  srgidcl  20344  srgidmlem  20346  issrgid  20349  srgpcomp  20363  srgpcompp  20364  srgpcomppsc  20365  srgbinomlem1  20371  srgbinomlem4  20374  srgbinomlem  20375  srgbinom  20376  csrgbinom  20377  ringcl  20395  crngcom  20396  iscrng2  20397  ringass  20398  ringideu  20399  crngbascntr  20401  ringidcl  20412  ringidmlem  20415  isringid  20418  ringidss  20424  isringrng  20434  ringpropd  20436  crngpropd  20437  isringd  20439  iscrngd  20440  ring1  20458  gsummgp0  20464  pwspjmhmmgpd  20474  pwsexpg  20475  pwsgprod  20476  xpsring1d  20480  oppr1  20497  unitgrpbas  20529  unitsubm  20533  rngidpropd  20562  isrnghmmul  20589  rnghmf1o  20599  idrnghm  20605  dfrhm2  20621  rhmmul  20637  isrhm2d  20638  idrhm  20642  rhmf1o  20644  pwsco1rhm  20658  pwsco2rhm  20659  c0rhm  20702  c0rnghm  20703  rhmimasubrnglem  20733  rhmimasubrng  20734  cntzsubrng  20735  subrgsubm  20753  issubrg3  20768  cntzsubr  20774  pwsdiagrhm  20775  rhmpropd  20777  isdomn3  20882  isdrng2  20912  isdrng3lem0  20919  isdrng3lem1  20920  drngid2  20925  isdrngd  20937  isdrngdOLD  20939  subrgacs  20972  cntzsdrg  20974  subdrgint  20975  primefld  20977  rlmscaf  21397  rnglidlmmgm  21448  rnglidlmsgrp  21449  rng2idl1cntr  21514  cringm4  21540  ssdifidlprm  21555  prmidlsubm  21556  xrsmcmn  21614  cnfldexp  21624  cnmsubglem  21649  expmhm  21655  nn0srg  21656  rge0srg  21657  expghm  21694  fermltlchr  21748  freshmansdream  21793  frobrhm  21794  cnmsgnbas  21797  sraassab  22089  assamulgscmlem1  22120  assamulgscmlem2  22121  psrcrng  22192  mplcoe3  22260  mplcoe5lem  22261  mplcoe5  22262  mplbas2  22264  evlslem3  22302  evlslem6  22303  evlslem1  22304  evlsvvvallem  22313  evlsvvval  22315  evlsgsummul  22319  evlspw  22320  mpfind  22337  evlsexpval  22350  selvvvval  22364  mhppwdeg  22384  psdpw  22404  ply1moncl  22503  coe1tm  22505  coe1pwmul  22511  ply1scltm  22513  ply1idvr1  22526  ply1coefsupp  22528  ply1coe  22529  gsummoncoe1  22539  lply1binomsc  22542  ply1fermltlchr  22543  evls1gsummul  22556  evls1pw  22557  evl1expd  22576  evl1gsummul  22591  evl1scvarpw  22594  evl1scvarpwval  22595  evl1gsummon  22596  evls1fpws  22600  rhmply1mon  22617  ringvcl  22628  mamuvs2  22634  matgsumcl  22688  madetsmelbas  22692  madetsmelbas2  22693  mat1mhm  22712  scmatmhm  22762  mdetleib2  22816  mdetf  22823  m1detdiag  22825  mdetdiaglem  22826  mdetdiag  22827  mdetdiagid  22828  mdetrlin  22830  mdetrsca  22831  mdetralt  22836  mdetunilem7  22846  mdetunilem8  22847  mdetuni0  22849  m2detleiblem2  22856  m2detleiblem3  22857  m2detleiblem4  22858  smadiadetlem4  22897  mat2pmatmhm  22964  pmatcollpwscmatlem1  23020  mply1topmatcllem  23034  mply1topmatcl  23036  pm2mpghm  23047  pm2mpmhm  23051  monmat2matmon  23055  pm2mp  23056  chpscmat  23073  chpscmatgsumbin  23075  chpscmatgsummon  23076  chp0mat  23077  chpidmat  23078  chfacfscmulcl  23088  chfacfscmul0  23089  chfacfscmulgsum  23091  chfacfpmmulcl  23092  chfacfpmmul0  23093  chfacfpmmulgsum  23095  chfacfpmmulgsum2  23096  cayhamlem1  23097  cpmadugsumlemB  23105  cpmadugsumlemC  23106  cpmadugsumlemF  23107  cayhamlem2  23115  cayhamlem4  23119  nrgtrg  24922  deg1pw  26353  ply1remlem  26397  fta1blem  26403  idomrootle  26405  plypf1  26445  efabl  26795  efsubm  26796  amgm  27235  wilthlem2  27313  wilthlem3  27314  dchrelbas2  27481  dchrelbas3  27482  dchrzrhmul  27490  dchrmulcl  27493  dchrn0  27494  dchrinvcl  27497  dchrfi  27499  dchrsum2  27512  sum2dchr  27518  lgsqrlem1  27590  lgsqrlem2  27591  lgsqrlem3  27592  lgsqrlem4  27593  lgseisenlem3  27621  lgseisenlem4  27622  dchrisum0flblem1  27752  zsoring  28682  cntrcrng  33529  psgnid  33545  cnmsgn0g  33594  altgnsg  33597  urpropd  33678  ringm1expp1  33681  isunit3  33688  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem3  33692  elrgspnlem4  33693  elrgspn  33694  elrgspnsubrunlem1  33695  elrgspnsubrunlem2  33696  0ringcring  33700  erlbr2d  33712  erler  33713  erld2  33714  rlocaddval  33717  rlocmulval  33718  rloccring  33719  rloc0g  33720  rloc1r  33721  rlocf1  33722  rlocinvunit  33723  rlocisunit  33724  domnprodn0  33726  domnprodeq0  33727  rrgsubm  33732  znfermltl  33809  unitprodclb  33830  ringlsmss  33834  lsmsnpridl  33837  mxidlprm  33881  rprmdvdspow  33951  rprmdvdsprod  33952  1arithidomlem1  33953  1arithidom  33955  1arithufdlem1  33962  1arithufdlem2  33963  1arithufdlem3  33964  1arithufdlem4  33965  dfufd2lem  33967  zringfrac  33972  ressply1evls1  33983  evl1deg1  33994  evl1deg2  33995  evl1deg3  33996  evls1monply1  33997  deg1prod  34001  ply1coedeg  34007  coe1vr1  34009  deg1vr  34010  gsummoncoe1fzo  34015  evlextv  34060  psrmonprod  34070  mplmonprod  34072  vietalem  34097  vieta  34098  srapwov  34107  ply1degltdimlem  34140  ply1degltdim  34141  assarrginv  34154  evls1fldgencl  34188  extdgfialglem1  34210  extdgfialglem2  34211  rtelextdg2lem  34244  2sqr3minply  34298  cos9thpiminplylem6  34305  cos9thpiminply  34306  mdetpmtr1  34341  iistmd  34420  xrge0iifmhm  34457  xrge0pluscn  34458  pl1cn  34473  zrhcntr  34497  aks6d1c1p2  42983  aks6d1c1p3  42984  aks6d1c1p4  42985  aks6d1c1p5  42986  aks6d1c1p7  42987  aks6d1c1p6  42988  aks6d1c1p8  42989  aks6d1c1  42990  evl1gprodd  42991  aks6d1c2lem4  43001  idomnnzpownz  43006  idomnnzgmulnz  43007  ringexp0nn  43008  aks6d1c5lem0  43009  aks6d1c5lem3  43011  aks6d1c5lem2  43012  aks6d1c5  43013  deg1gprod  43014  deg1pow  43015  aks6d1c6lem1  43044  aks6d1c6lem2  43045  aks6d1c6lem3  43046  aks5lem2  43061  aks5lem3a  43063  unitscyglem5  43073  aks5lem7  43074  domnexpgn0cl  43413  abvexp  43422  fidomncyc  43425  evlselv  43443  mhphf  43451  hbtlem4  43975  mon1psubm  44048  deg1mhm  44049  amgm2d  45046  amgm3d  45047  amgm4d  45048  2zrngmmgm  49175  2zrngmsgrp  49176  2zrngnring  49181  cznrng  49184  cznnring  49185  mgpsumunsn  49299  mgpsumz  49300  mgpsumn  49301  invginvrid  49305  ply1vr1smo  49321  ply1mulgsumlem4  49327  ply1mulgsum  49328  elmgpcntrd  49939  amgmlemALT  50829  amgmw2d  50830