Theorem mgpbas 20398

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 2763	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20396	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17422	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17490	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19597	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2786	1 ⊢ 𝐵 = (Base‘𝑀)

This proof depends on syntax axioms:   = wceq 1570  ‘cfv 6561  Basecbs 17419  ._rcmulr 17461  mulGrpcmgp 20393

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-cnex 11286  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-nn 12366  df-2 12435  df-sets 17374  df-slot 17392  df-ndx 17404  df-base 17420  df-plusg 17473  df-mgp 20394

This theorem is used by:  mgptopn  20401  mgpress  20403  prdsmgp  20404  elmgplsm  20405  rngass  20414  rngcl  20419  isrngd  20428  rngpropd  20429  rng1zrlem  20436  dfur2  20443  srgcl  20452  srgass  20453  srgideu  20454  srgidcl  20458  srgidmlem  20460  issrgid  20463  srgpcomp  20477  srgpcompp  20478  srgpcomppsc  20479  srgbinomlem1  20485  srgbinomlem4  20488  srgbinomlem  20489  srgbinom  20490  csrgbinom  20491  ringcl  20510  crngcom  20511  iscrng2  20512  ringass  20513  ringideu  20514  crngbascntr  20516  ringidcl  20527  ringidmlem  20530  isringid  20533  ringidss  20539  isringrng  20549  dfring3  20551  ringpropd  20552  crngpropd  20553  isringd  20555  iscrngd  20556  ring1  20574  gsummgp0  20580  pwspjmhmmgpd  20590  pwsexpg  20591  pwsgprod  20592  xpsring1d  20596  oppr1  20613  unitgrpbas  20645  unitsubm  20649  rngidpropd  20678  isrnghmmul  20705  rnghmf1o  20715  idrnghm  20721  dfrhm2  20737  rhmmul  20753  isrhm2d  20754  idrhm  20758  rhmf1o  20760  pwsco1rhm  20774  pwsco2rhm  20775  c0rhm  20819  c0rnghm  20820  rhmimasubrnglem  20850  rhmimasubrng  20851  cntzsubrng  20852  subrgsubm  20870  issubrg3  20885  cntzsubr  20891  pwsdiagrhm  20892  rhmpropd  20894  isdomn3  20999  isdrng2  21030  isdrng3lem0  21037  isdrng3lem1  21038  drngid2  21043  isdrngd  21055  isdrngdOLD  21057  subrgacs  21090  cntzsdrg  21092  subdrgint  21093  primefld  21095  rlmscaf  21515  rnglidlmmgm  21566  rnglidlmsgrp  21567  rng2idl1cntr  21634  cringm4  21660  ssdifidlprm  21675  prmidlsubm  21676  xrsmcmn  21734  cnfldexp  21744  cnmsubglem  21769  expmhm  21775  nn0srg  21776  rge0srg  21777  expghm  21814  fermltlchr  21868  freshmansdream  21913  frobrhm  21914  cnmsgnbas  21917  sraassab  22209  assamulgscmlem1  22240  assamulgscmlem2  22241  psrcrng  22312  mplcoe3  22380  mplcoe5lem  22381  mplcoe5  22382  mplbas2  22384  evlslem3  22422  evlslem6  22423  evlslem1  22424  evlsvvvallem  22433  evlsvvval  22435  evlsgsummul  22439  evlspw  22440  mpfind  22457  evlsexpval  22470  selvvvval  22484  mhppwdeg  22504  psdpw  22524  ply1moncl  22623  coe1tm  22625  coe1pwmul  22631  ply1scltm  22633  ply1idvr1  22646  ply1coefsupp  22648  ply1coe  22649  gsummoncoe1  22659  lply1binomsc  22662  ply1fermltlchr  22663  evls1gsummul  22676  evls1pw  22677  evl1expd  22696  evl1gsummul  22711  evl1scvarpw  22714  evl1scvarpwval  22715  evl1gsummon  22716  evls1fpws  22720  rhmply1mon  22737  ringvcl  22748  mamuvs2  22754  matgsumcl  22808  madetsmelbas  22812  madetsmelbas2  22813  mat1mhm  22832  scmatmhm  22882  mdetleib2  22936  mdetf  22943  m1detdiag  22945  mdetdiaglem  22946  mdetdiag  22947  mdetdiagid  22948  mdetrlin  22950  mdetrsca  22951  mdetralt  22956  mdetunilem7  22966  mdetunilem8  22967  mdetuni0  22969  m2detleiblem2  22976  m2detleiblem3  22977  m2detleiblem4  22978  smadiadetlem4  23017  mat2pmatmhm  23084  pmatcollpwscmatlem1  23140  mply1topmatcllem  23154  mply1topmatcl  23156  pm2mpghm  23167  pm2mpmhm  23171  monmat2matmon  23175  pm2mp  23176  chpscmat  23193  chpscmatgsumbin  23195  chpscmatgsummon  23196  chp0mat  23197  chpidmat  23198  chfacfscmulcl  23208  chfacfscmul0  23209  chfacfscmulgsum  23211  chfacfpmmulcl  23212  chfacfpmmul0  23213  chfacfpmmulgsum  23215  chfacfpmmulgsum2  23216  cayhamlem1  23217  cpmadugsumlemB  23225  cpmadugsumlemC  23226  cpmadugsumlemF  23227  cayhamlem2  23235  cayhamlem4  23239  nrgtrg  25042  deg1pw  26472  ply1remlem  26516  fta1blem  26522  idomrootle  26524  plypf1  26564  efabl  26911  efsubm  26912  amgm  27351  wilthlem2  27429  wilthlem3  27430  dchrelbas2  27597  dchrelbas3  27598  dchrzrhmul  27606  dchrmulcl  27609  dchrn0  27610  dchrinvcl  27613  dchrfi  27615  dchrsum2  27628  sum2dchr  27634  lgsqrlem1  27706  lgsqrlem2  27707  lgsqrlem3  27708  lgsqrlem4  27709  lgseisenlem3  27737  lgseisenlem4  27738  dchrisum0flblem1  27868  zsoring  28828  cntrcrng  33718  psgnid  33734  cnmsgn0g  33783  altgnsg  33786  urpropd  33867  ringm1expp1  33870  isunit3  33877  elrgspnlem1  33879  elrgspnlem2  33880  elrgspnlem3  33881  elrgspnlem4  33882  elrgspn  33883  elrgspnsubrunlem1  33884  elrgspnsubrunlem2  33885  0ringcring  33889  erlbr2d  33901  erler  33902  erld2  33903  rlocaddval  33906  rlocmulval  33907  rloccring  33908  rloc0g  33909  rloc1r  33910  rlocf1  33911  rlocinvunit  33912  rlocisunit  33913  domnprodn0  33915  domnprodeq0  33916  rrgsubm  33921  znfermltl  34006  unitprodclb  34028  ringlsmss  34032  lsmsnpridl  34035  mxidlprm  34079  rprmdvdspow  34149  rprmdvdsprod  34150  1arithidomlem1  34151  1arithidom  34153  1arithufdlem1  34160  1arithufdlem2  34161  1arithufdlem3  34162  1arithufdlem4  34163  dfufd2lem  34165  zringfrac  34169  ressply1evls1  34180  evl1deg1  34191  evl1deg2  34192  evl1deg3  34193  evls1monply1  34194  deg1prod  34198  ply1coedeg  34204  coe1vr1  34206  deg1vr  34207  gsummoncoe1fzo  34212  evlextv  34257  psrmonprod  34267  mplmonprod  34269  vietalem  34294  vieta  34295  srapwov  34304  ply1degltdimlem  34337  ply1degltdim  34338  assarrginv  34351  evls1fldgencl  34385  extdgfialglem1  34407  extdgfialglem2  34408  rtelextdg2lem  34441  2sqr3minply  34495  cos9thpiminplylem6  34502  cos9thpiminply  34503  mdetpmtr1  34538  iistmd  34617  xrge0iifmhm  34654  xrge0pluscn  34655  pl1cn  34670  zrhcntr  34694  aks6d1c1p2  43362  aks6d1c1p3  43363  aks6d1c1p4  43364  aks6d1c1p5  43365  aks6d1c1p7  43366  aks6d1c1p6  43367  aks6d1c1p8  43368  aks6d1c1  43369  evl1gprodd  43370  aks6d1c2lem4  43380  idomnnzpownz  43385  idomnnzgmulnz  43386  ringexp0nn  43387  aks6d1c5lem0  43388  aks6d1c5lem3  43390  aks6d1c5lem2  43391  aks6d1c5  43392  deg1gprod  43393  deg1pow  43394  aks6d1c6lem1  43423  aks6d1c6lem2  43424  aks6d1c6lem3  43425  aks5lem2  43440  aks5lem3a  43442  unitscyglem5  43452  aks5lem7  43453  domnexpgn0cl  43788  abvexp  43800  fidomncyc  43803  evlselv  43821  mhphf  43829  hbtlem4  44331  mon1psubm  44404  deg1mhm  44405  amgm2d  45401  amgm3d  45402  amgm4d  45403  2zrngmmgm  49564  2zrngmsgrp  49565  2zrngnring  49570  cznrng  49573  cznnring  49574  mgpsumunsn  49688  mgpsumz  49689  mgpsumn  49690  invginvrid  49694  ply1vr1smo  49710  ply1mulgsumlem4  49716  ply1mulgsum  49717  elmgpcntrd  50334  amgmlemALT  51300  amgmw2d  51301