Theorem mgpbas 20252

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 2766	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20250	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17297	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17365	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19451	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2789	1 ⊢ 𝐵 = (Base‘𝑀)

This proof depends on syntax axioms:   = wceq 1570  ‘cfv 6543  Basecbs 17294  ._rcmulr 17336  mulGrpcmgp 20247

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-nn 12252  df-2 12321  df-sets 17249  df-slot 17267  df-ndx 17279  df-base 17295  df-plusg 17348  df-mgp 20248

This theorem is used by:  mgptopn  20255  mgpress  20257  prdsmgp  20258  elmgplsm  20259  rngass  20268  rngcl  20273  isrngd  20282  rngpropd  20283  rng1zrlem  20290  dfur2  20297  srgcl  20306  srgass  20307  srgideu  20308  srgidcl  20312  srgidmlem  20314  issrgid  20317  srgpcomp  20331  srgpcompp  20332  srgpcomppsc  20333  srgbinomlem1  20339  srgbinomlem4  20342  srgbinomlem  20343  srgbinom  20344  csrgbinom  20345  ringcl  20363  crngcom  20364  iscrng2  20365  ringass  20366  ringideu  20367  crngbascntr  20369  ringidcl  20380  ringidmlem  20383  isringid  20386  ringidss  20392  isringrng  20402  ringpropd  20404  crngpropd  20405  isringd  20407  iscrngd  20408  ring1  20426  gsummgp0  20432  pwspjmhmmgpd  20442  pwsexpg  20443  pwsgprod  20444  xpsring1d  20448  oppr1  20465  unitgrpbas  20497  unitsubm  20501  rngidpropd  20530  isrnghmmul  20557  rnghmf1o  20567  idrnghm  20573  dfrhm2  20589  rhmmul  20605  isrhm2d  20606  idrhm  20610  rhmf1o  20612  pwsco1rhm  20626  pwsco2rhm  20627  c0rhm  20670  c0rnghm  20671  rhmimasubrnglem  20701  rhmimasubrng  20702  cntzsubrng  20703  subrgsubm  20721  issubrg3  20736  cntzsubr  20742  pwsdiagrhm  20743  rhmpropd  20745  isdomn3  20850  isdrng2  20880  isdrng3lem0  20887  isdrng3lem1  20888  drngid2  20893  isdrngd  20905  isdrngdOLD  20907  subrgacs  20940  cntzsdrg  20942  subdrgint  20943  primefld  20945  rlmscaf  21365  rnglidlmmgm  21416  rnglidlmsgrp  21417  rng2idl1cntr  21482  cringm4  21508  ssdifidlprm  21523  prmidlsubm  21524  xrsmcmn  21582  cnfldexp  21592  cnmsubglem  21617  expmhm  21623  nn0srg  21624  rge0srg  21625  expghm  21662  fermltlchr  21716  freshmansdream  21761  frobrhm  21762  cnmsgnbas  21765  sraassab  22055  assamulgscmlem1  22086  assamulgscmlem2  22087  psrcrng  22158  mplcoe3  22226  mplcoe5lem  22227  mplcoe5  22228  mplbas2  22230  evlslem3  22268  evlslem6  22269  evlslem1  22270  evlsvvvallem  22279  evlsvvval  22281  evlsgsummul  22285  evlspw  22286  mpfind  22303  evlsexpval  22316  selvvvval  22330  mhppwdeg  22350  psdpw  22370  ply1moncl  22469  coe1tm  22471  coe1pwmul  22477  ply1scltm  22479  ply1idvr1  22492  ply1coefsupp  22494  ply1coe  22495  gsummoncoe1  22505  lply1binomsc  22508  ply1fermltlchr  22509  evls1gsummul  22522  evls1pw  22523  evl1expd  22542  evl1gsummul  22557  evl1scvarpw  22560  evl1scvarpwval  22561  evl1gsummon  22562  evls1fpws  22566  rhmply1mon  22583  ringvcl  22594  mamuvs2  22600  matgsumcl  22654  madetsmelbas  22658  madetsmelbas2  22659  mat1mhm  22678  scmatmhm  22728  mdetleib2  22782  mdetf  22789  m1detdiag  22791  mdetdiaglem  22792  mdetdiag  22793  mdetdiagid  22794  mdetrlin  22796  mdetrsca  22797  mdetralt  22802  mdetunilem7  22812  mdetunilem8  22813  mdetuni0  22815  m2detleiblem2  22822  m2detleiblem3  22823  m2detleiblem4  22824  smadiadetlem4  22863  mat2pmatmhm  22927  pmatcollpwscmatlem1  22983  mply1topmatcllem  22997  mply1topmatcl  22999  pm2mpghm  23010  pm2mpmhm  23014  monmat2matmon  23018  pm2mp  23019  chpscmat  23036  chpscmatgsumbin  23038  chpscmatgsummon  23039  chp0mat  23040  chpidmat  23041  chfacfscmulcl  23051  chfacfscmul0  23052  chfacfscmulgsum  23054  chfacfpmmulcl  23055  chfacfpmmul0  23056  chfacfpmmulgsum  23058  chfacfpmmulgsum2  23059  cayhamlem1  23060  cpmadugsumlemB  23068  cpmadugsumlemC  23069  cpmadugsumlemF  23070  cayhamlem2  23078  cayhamlem4  23082  nrgtrg  24884  deg1pw  26315  ply1remlem  26359  fta1blem  26365  idomrootle  26367  plypf1  26406  efabl  26752  efsubm  26753  amgm  27192  wilthlem2  27270  wilthlem3  27271  dchrelbas2  27438  dchrelbas3  27439  dchrzrhmul  27447  dchrmulcl  27450  dchrn0  27451  dchrinvcl  27454  dchrfi  27456  dchrsum2  27469  sum2dchr  27475  lgsqrlem1  27547  lgsqrlem2  27548  lgsqrlem3  27549  lgsqrlem4  27550  lgseisenlem3  27578  lgseisenlem4  27579  dchrisum0flblem1  27709  zsoring  28639  cntrcrng  33432  psgnid  33448  cnmsgn0g  33497  altgnsg  33500  urpropd  33581  ringm1expp1  33584  isunit3  33591  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem3  33595  elrgspnlem4  33596  elrgspn  33597  elrgspnsubrunlem1  33598  elrgspnsubrunlem2  33599  0ringcring  33603  erlbr2d  33615  erler  33616  erld2  33617  rlocaddval  33620  rlocmulval  33621  rloccring  33622  rloc0g  33623  rloc1r  33624  rlocf1  33625  rlocinvunit  33626  rlocisunit  33627  domnprodn0  33629  domnprodeq0  33630  rrgsubm  33635  znfermltl  33712  unitprodclb  33733  ringlsmss  33737  lsmsnpridl  33740  mxidlprm  33784  rprmdvdspow  33854  rprmdvdsprod  33855  1arithidomlem1  33856  1arithidom  33858  1arithufdlem1  33865  1arithufdlem2  33866  1arithufdlem3  33867  1arithufdlem4  33868  dfufd2lem  33870  zringfrac  33875  ressply1evls1  33886  evl1deg1  33897  evl1deg2  33898  evl1deg3  33899  evls1monply1  33900  deg1prod  33904  ply1coedeg  33910  coe1vr1  33912  deg1vr  33913  gsummoncoe1fzo  33918  evlextv  33963  psrmonprod  33973  mplmonprod  33975  vietalem  34000  vieta  34001  srapwov  34010  ply1degltdimlem  34043  ply1degltdim  34044  assarrginv  34057  evls1fldgencl  34091  extdgfialglem1  34113  extdgfialglem2  34114  rtelextdg2lem  34147  2sqr3minply  34201  cos9thpiminplylem6  34208  cos9thpiminply  34209  mdetpmtr1  34244  iistmd  34323  xrge0iifmhm  34360  xrge0pluscn  34361  pl1cn  34376  zrhcntr  34400  aks6d1c1p2  42917  aks6d1c1p3  42918  aks6d1c1p4  42919  aks6d1c1p5  42920  aks6d1c1p7  42921  aks6d1c1p6  42922  aks6d1c1p8  42923  aks6d1c1  42924  evl1gprodd  42925  aks6d1c2lem4  42935  idomnnzpownz  42940  idomnnzgmulnz  42941  ringexp0nn  42942  aks6d1c5lem0  42943  aks6d1c5lem3  42945  aks6d1c5lem2  42946  aks6d1c5  42947  deg1gprod  42948  deg1pow  42949  aks6d1c6lem1  42978  aks6d1c6lem2  42979  aks6d1c6lem3  42980  aks5lem2  42995  aks5lem3a  42997  unitscyglem5  43007  aks5lem7  43008  domnexpgn0cl  43332  abvexp  43341  fidomncyc  43344  evlselv  43362  mhphf  43370  hbtlem4  43894  mon1psubm  43967  deg1mhm  43968  amgm2d  44965  amgm3d  44966  amgm4d  44967  2zrngmmgm  49058  2zrngmsgrp  49059  2zrngnring  49064  cznrng  49067  cznnring  49068  mgpsumunsn  49182  mgpsumz  49183  mgpsumn  49184  invginvrid  49188  ply1vr1smo  49204  ply1mulgsumlem4  49210  ply1mulgsum  49211  elmgpcntrd  49824  amgmlemALT  50692  amgmw2d  50693