Theorem mgpbas 20174

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 2761	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
4	2, 3	mgpval 20172	. . 3 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), (.r‘𝑅)⟩)
5		baseid 17231	. . 3 ⊢ Base = Slot (Base‘ndx)
6		basendxnplusgndx 17299	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
7	4, 5, 6	setsplusg 19373	. 2 ⊢ (Base‘𝑅) = (Base‘𝑀)
8	1, 7	eqtri 2784	1 ⊢ 𝐵 = (Base‘𝑀)

Syntax hints:   = wceq 1559  ‘cfv 6517  Basecbs 17228  ._rcmulr 17270  mulGrpcmgp 20169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-cnex 11126  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-om 7843  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-nn 12208  df-2 12277  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17229  df-plusg 17282  df-mgp 20170

This theorem is referenced by:  mgptopn  20177  mgpress  20179  prdsmgp  20180  rngass  20188  rngcl  20193  isrngd  20202  rngpropd  20203  dfur2  20213  srgcl  20222  srgass  20223  srgideu  20224  srgidcl  20228  srgidmlem  20230  issrgid  20233  srg1zr  20244  srgpcomp  20247  srgpcompp  20248  srgpcomppsc  20249  srgbinomlem1  20255  srgbinomlem4  20258  srgbinomlem  20259  srgbinom  20260  csrgbinom  20261  ringcl  20279  crngcom  20280  iscrng2  20281  ringass  20282  ringideu  20283  crngbascntr  20285  ringidcl  20294  ringidmlem  20297  isringid  20300  ringidss  20306  isringrng  20316  ringpropd  20317  crngpropd  20318  isringd  20320  iscrngd  20321  ring1  20339  gsummgp0  20345  pwspjmhmmgpd  20355  pwsexpg  20356  pwsgprod  20357  xpsring1d  20361  oppr1  20378  unitgrpbas  20410  unitsubm  20414  rngidpropd  20443  isrnghmmul  20470  rnghmf1o  20480  idrnghm  20486  dfrhm2  20502  rhmmul  20514  isrhm2d  20515  idrhm  20518  rhmf1o  20519  pwsco1rhm  20530  pwsco2rhm  20531  c0rhm  20563  c0rnghm  20564  rhmimasubrnglem  20594  rhmimasubrng  20595  cntzsubrng  20596  subrgsubm  20614  issubrg3  20629  cntzsubr  20635  pwsdiagrhm  20636  rhmpropd  20638  isdomn3  20744  isdrng2  20772  drngmclOLD  20780  drngid2  20781  isdrngd  20794  isdrngdOLD  20796  subrgacs  20829  cntzsdrg  20831  subdrgint  20832  primefld  20834  rlmscaf  21254  rnglidlmmgm  21295  rnglidlmsgrp  21296  rng2idl1cntr  21355  xrsmcmn  21427  cnfldexp  21437  cnmsubglem  21462  expmhm  21468  nn0srg  21469  rge0srg  21470  expghm  21507  fermltlchr  21561  freshmansdream  21606  frobrhm  21607  cnmsgnbas  21610  sraassab  21900  assamulgscmlem1  21931  assamulgscmlem2  21932  psrcrng  22003  mplcoe3  22071  mplcoe5lem  22072  mplcoe5  22073  mplbas2  22075  evlslem3  22113  evlslem6  22114  evlslem1  22115  evlsvvvallem  22124  evlsvvval  22126  evlsgsummul  22130  evlspw  22131  mpfind  22148  evlsexpval  22161  selvvvval  22175  mhppwdeg  22195  psdpw  22215  ply1moncl  22314  coe1tm  22316  coe1pwmul  22322  ply1scltm  22324  ply1idvr1  22337  ply1coefsupp  22340  ply1coe  22341  gsummoncoe1  22351  lply1binomsc  22354  ply1fermltlchr  22355  evls1gsummul  22368  evls1pw  22369  evl1expd  22388  evl1gsummul  22403  evl1scvarpw  22406  evl1scvarpwval  22407  evl1gsummon  22408  evls1fpws  22412  rhmply1mon  22429  ringvcl  22440  mamuvs2  22446  matgsumcl  22500  madetsmelbas  22504  madetsmelbas2  22505  mat1mhm  22524  scmatmhm  22574  mdetleib2  22628  mdetf  22635  m1detdiag  22637  mdetdiaglem  22638  mdetdiag  22639  mdetdiagid  22640  mdetrlin  22642  mdetrsca  22643  mdetralt  22648  mdetunilem7  22658  mdetunilem8  22659  mdetuni0  22661  m2detleiblem2  22668  m2detleiblem3  22669  m2detleiblem4  22670  smadiadetlem4  22709  mat2pmatmhm  22773  pmatcollpwscmatlem1  22829  mply1topmatcllem  22843  mply1topmatcl  22845  pm2mpghm  22856  pm2mpmhm  22860  monmat2matmon  22864  pm2mp  22865  chpscmat  22882  chpscmatgsumbin  22884  chpscmatgsummon  22885  chp0mat  22886  chpidmat  22887  chfacfscmulcl  22897  chfacfscmul0  22898  chfacfscmulgsum  22900  chfacfpmmulcl  22901  chfacfpmmul0  22902  chfacfpmmulgsum  22904  chfacfpmmulgsum2  22905  cayhamlem1  22906  cpmadugsumlemB  22914  cpmadugsumlemC  22915  cpmadugsumlemF  22916  cayhamlem2  22924  cayhamlem4  22928  nrgtrg  24730  deg1pw  26161  ply1remlem  26205  fta1blem  26211  idomrootle  26213  plypf1  26252  efabl  26592  efsubm  26593  amgm  27032  wilthlem2  27110  wilthlem3  27111  dchrelbas2  27278  dchrelbas3  27279  dchrzrhmul  27287  dchrmulcl  27290  dchrn0  27291  dchrinvcl  27294  dchrfi  27296  dchrsum2  27309  sum2dchr  27315  lgsqrlem1  27387  lgsqrlem2  27388  lgsqrlem3  27389  lgsqrlem4  27390  lgseisenlem3  27418  lgseisenlem4  27419  dchrisum0flblem1  27549  zsoring  28479  cntrcrng  33222  psgnid  33238  cnmsgn0g  33287  altgnsg  33290  urpropd  33372  ringm1expp1  33375  isunit3  33382  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  elrgspn  33388  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  0ringcring  33394  erlbr2d  33406  erler  33407  erld2  33408  rlocaddval  33411  rlocmulval  33412  rloccring  33413  rloc0g  33414  rloc1r  33415  rlocf1  33416  rlocinvunit  33417  rlocisunit  33418  domnprodn0  33420  domnprodeq0  33421  rrgsubm  33429  znfermltl  33513  unitprodclb  33536  elringlsm  33540  ringlsmss  33542  lsmsnpridl  33545  cringm4  33593  ssdifidlprm  33606  prmidlsubm  33607  mxidlprm  33619  rprmdvdspow  33690  rprmdvdsprod  33691  1arithidomlem1  33692  1arithidom  33694  1arithufdlem1  33701  1arithufdlem2  33702  1arithufdlem3  33703  1arithufdlem4  33704  dfufd2lem  33706  zringfrac  33711  ressply1evls1  33722  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  evls1monply1  33736  deg1prod  33740  ply1coedeg  33746  coe1vr1  33748  deg1vr  33749  gsummoncoe1fzo  33754  evlextv  33800  psrmonprod  33810  mplmonprod  33812  vietalem  33837  vieta  33838  srapwov  33847  ply1degltdimlem  33880  ply1degltdim  33881  assarrginv  33894  evls1fldgencl  33928  extdgfialglem1  33950  extdgfialglem2  33951  rtelextdg2lem  33984  2sqr3minply  34038  cos9thpiminplylem6  34045  cos9thpiminply  34046  mdetpmtr1  34081  iistmd  34160  xrge0iifmhm  34197  xrge0pluscn  34198  pl1cn  34213  zrhcntr  34237  aks6d1c1p2  42690  aks6d1c1p3  42691  aks6d1c1p4  42692  aks6d1c1p5  42693  aks6d1c1p7  42694  aks6d1c1p6  42695  aks6d1c1p8  42696  aks6d1c1  42697  evl1gprodd  42698  aks6d1c2lem4  42708  idomnnzpownz  42713  idomnnzgmulnz  42714  ringexp0nn  42715  aks6d1c5lem0  42716  aks6d1c5lem3  42718  aks6d1c5lem2  42719  aks6d1c5  42720  deg1gprod  42721  deg1pow  42722  aks6d1c6lem1  42751  aks6d1c6lem2  42752  aks6d1c6lem3  42753  aks5lem2  42768  aks5lem3a  42770  unitscyglem5  42780  aks5lem7  42781  domnexpgn0cl  43105  abvexp  43114  fidomncyc  43117  evlselv  43135  mhphf  43143  hbtlem4  43667  mon1psubm  43740  deg1mhm  43741  amgm2d  44738  amgm3d  44739  amgm4d  44740  2zrngmmgm  48838  2zrngmsgrp  48839  2zrngnring  48844  cznrng  48847  cznnring  48848  mgpsumunsn  48947  mgpsumz  48948  mgpsumn  48949  invginvrid  48953  ply1vr1smo  48969  ply1mulgsumlem4  48975  ply1mulgsum  48976  elmgpcntrd  49590  amgmlemALT  50388  amgmw2d  50389