Theorem mgpbas 20126

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 2736	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20124	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17182	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17250	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19325	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2759	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1542  ‘cfv 6498  Basecbs 17179  ._rcmulr 17221  mulGrpcmgp 20121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-2 12244  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-plusg 17233  df-mgp 20122

This theorem is referenced by:  mgptopn  20129  mgpress  20131  prdsmgp  20132  rngass  20140  rngcl  20145  isrngd  20154  rngpropd  20155  dfur2  20165  srgcl  20174  srgass  20175  srgideu  20176  srgidcl  20180  srgidmlem  20182  issrgid  20185  srg1zr  20196  srgpcomp  20199  srgpcompp  20200  srgpcomppsc  20201  srgbinomlem1  20207  srgbinomlem4  20210  srgbinomlem  20211  srgbinom  20212  csrgbinom  20213  ringcl  20231  crngcom  20232  iscrng2  20233  ringass  20234  ringideu  20235  crngbascntr  20237  ringidcl  20246  ringidmlem  20249  isringid  20252  ringidss  20258  isringrng  20268  ringpropd  20269  crngpropd  20270  isringd  20272  iscrngd  20273  ring1  20291  gsummgp0  20297  pwspjmhmmgpd  20307  pwsexpg  20308  pwsgprod  20309  xpsring1d  20313  oppr1  20330  unitgrpbas  20362  unitsubm  20366  rngidpropd  20395  isrnghmmul  20422  rnghmf1o  20432  idrnghm  20438  dfrhm2  20454  rhmmul  20465  isrhm2d  20466  idrhm  20469  rhmf1o  20470  pwsco1rhm  20479  pwsco2rhm  20480  c0rhm  20511  c0rnghm  20512  rhmimasubrnglem  20542  rhmimasubrng  20543  cntzsubrng  20544  subrgsubm  20562  issubrg3  20577  cntzsubr  20583  pwsdiagrhm  20584  rhmpropd  20586  isdomn3  20692  isdrng2  20720  drngmclOLD  20728  drngid2  20729  isdrngd  20742  isdrngdOLD  20744  subrgacs  20777  cntzsdrg  20779  subdrgint  20780  primefld  20782  rlmscaf  21202  rnglidlmmgm  21243  rnglidlmsgrp  21244  rng2idl1cntr  21303  xrsmcmn  21375  cnfldexp  21385  cnmsubglem  21410  expmhm  21416  nn0srg  21417  rge0srg  21418  expghm  21455  fermltlchr  21509  freshmansdream  21554  frobrhm  21555  cnmsgnbas  21558  sraassab  21848  assamulgscmlem1  21879  assamulgscmlem2  21880  psrcrng  21950  mplcoe3  22016  mplcoe5lem  22017  mplcoe5  22018  mplbas2  22020  evlslem3  22058  evlslem6  22059  evlslem1  22060  evlsvvvallem  22069  evlsvvval  22071  evlsgsummul  22075  evlspw  22076  mpfind  22093  mhppwdeg  22116  psdpw  22136  ply1moncl  22236  coe1tm  22238  coe1pwmul  22244  ply1scltm  22246  ply1idvr1  22259  ply1coefsupp  22262  ply1coe  22263  gsummoncoe1  22273  lply1binomsc  22276  ply1fermltlchr  22277  evls1gsummul  22290  evls1pw  22291  evl1expd  22310  evl1gsummul  22325  evl1scvarpw  22328  evl1scvarpwval  22329  evl1gsummon  22330  evls1fpws  22334  rhmply1mon  22354  ringvcl  22365  mamuvs2  22371  matgsumcl  22425  madetsmelbas  22429  madetsmelbas2  22430  mat1mhm  22449  scmatmhm  22499  mdetleib2  22553  mdetf  22560  m1detdiag  22562  mdetdiaglem  22563  mdetdiag  22564  mdetdiagid  22565  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  mdetunilem7  22583  mdetunilem8  22584  mdetuni0  22586  m2detleiblem2  22593  m2detleiblem3  22594  m2detleiblem4  22595  smadiadetlem4  22634  mat2pmatmhm  22698  pmatcollpwscmatlem1  22754  mply1topmatcllem  22768  mply1topmatcl  22770  pm2mpghm  22781  pm2mpmhm  22785  monmat2matmon  22789  pm2mp  22790  chpscmat  22807  chpscmatgsumbin  22809  chpscmatgsummon  22810  chp0mat  22811  chpidmat  22812  chfacfscmulcl  22822  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmulcl  22826  chfacfpmmul0  22827  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cayhamlem2  22849  cayhamlem4  22853  nrgtrg  24655  deg1pw  26086  ply1remlem  26130  fta1blem  26136  idomrootle  26138  plypf1  26177  efabl  26514  efsubm  26515  amgm  26954  wilthlem2  27032  wilthlem3  27033  dchrelbas2  27200  dchrelbas3  27201  dchrzrhmul  27209  dchrmulcl  27212  dchrn0  27213  dchrinvcl  27216  dchrfi  27218  dchrsum2  27231  sum2dchr  27237  lgsqrlem1  27309  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  lgseisenlem3  27340  lgseisenlem4  27341  dchrisum0flblem1  27471  zsoring  28401  cntrcrng  33142  psgnid  33158  cnmsgn0g  33207  altgnsg  33210  urpropd  33292  ringm1expp1  33295  isunit3  33302  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  0ringcring  33313  erlbr2d  33325  erler  33326  rlocaddval  33329  rlocmulval  33330  rloccring  33331  rloc0g  33332  rloc1r  33333  rlocf1  33334  domnprodn0  33336  domnprodeq0  33337  rrgsubm  33345  znfermltl  33426  unitprodclb  33449  elringlsm  33453  ringlsmss  33455  lsmsnpridl  33458  cringm4  33506  ssdifidlprm  33518  mxidlprm  33530  rprmdvdspow  33593  rprmdvdsprod  33594  1arithidomlem1  33595  1arithidom  33597  1arithufdlem1  33604  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  zringfrac  33614  ressply1evls1  33625  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  evls1monply1  33639  deg1prod  33643  ply1coedeg  33649  coe1vr1  33651  deg1vr  33652  gsummoncoe1fzo  33657  evlextv  33686  psrmonprod  33696  mplmonprod  33698  vietalem  33723  vieta  33724  srapwov  33733  ply1degltdimlem  33766  ply1degltdim  33767  assarrginv  33780  evls1fldgencl  33814  extdgfialglem1  33836  extdgfialglem2  33837  rtelextdg2lem  33870  2sqr3minply  33924  cos9thpiminplylem6  33931  cos9thpiminply  33932  mdetpmtr1  33967  iistmd  34046  xrge0iifmhm  34083  xrge0pluscn  34084  pl1cn  34099  zrhcntr  34123  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1p7  42552  aks6d1c1p6  42553  aks6d1c1p8  42554  aks6d1c1  42555  evl1gprodd  42556  aks6d1c2lem4  42566  idomnnzpownz  42571  idomnnzgmulnz  42572  ringexp0nn  42573  aks6d1c5lem0  42574  aks6d1c5lem3  42576  aks6d1c5lem2  42577  aks6d1c5  42578  deg1gprod  42579  deg1pow  42580  aks6d1c6lem1  42609  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks5lem2  42626  aks5lem3a  42628  unitscyglem5  42638  aks5lem7  42639  domnexpgn0cl  42968  abvexp  42977  fidomncyc  42980  evlsexpval  43003  selvvvval  43018  evlselv  43020  mhphf  43030  hbtlem4  43554  mon1psubm  43627  deg1mhm  43628  amgm2d  44625  amgm3d  44626  amgm4d  44627  2zrngmmgm  48728  2zrngmsgrp  48729  2zrngnring  48734  cznrng  48737  cznnring  48738  mgpsumunsn  48837  mgpsumz  48838  mgpsumn  48839  invginvrid  48843  ply1vr1smo  48859  ply1mulgsumlem4  48865  ply1mulgsum  48866  elmgpcntrd  49480  amgmlemALT  50278  amgmw2d  50279