MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpinvcl Structured version   Visualization version   GIF version

Theorem grpinvcl 18147
Description: A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.)
Hypotheses
Ref Expression
grpinvcl.b 𝐵 = (Base‘𝐺)
grpinvcl.n 𝑁 = (invg𝐺)
Assertion
Ref Expression
grpinvcl ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)

Proof of Theorem grpinvcl
StepHypRef Expression
1 grpinvcl.b . . 3 𝐵 = (Base‘𝐺)
2 grpinvcl.n . . 3 𝑁 = (invg𝐺)
31, 2grpinvf 18146 . 2 (𝐺 ∈ Grp → 𝑁:𝐵𝐵)
43ffvelrnda 6832 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2112  cfv 6328  Basecbs 16479  Grpcgrp 18099  invgcminusg 18100
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336  df-riota 7097  df-ov 7142  df-0g 16711  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-grp 18102  df-minusg 18103
This theorem is referenced by:  grprinv  18149  grpinvid1  18150  grpinvid2  18151  grplrinv  18153  grplcan  18157  grpasscan1  18158  grpasscan2  18159  grpinvinv  18162  grpinvcnv  18163  grpinvnzcl  18167  grpsubinv  18168  grplmulf1o  18169  grpinvssd  18172  grpinvadd  18173  grpsubf  18174  grpsubrcan  18176  grpinvsub  18177  grpinvval2  18178  grpsubeq0  18181  grpsubadd  18183  grpaddsubass  18185  grpnpcan  18187  dfgrp3  18194  grplactcnv  18198  grpsubpropd2  18201  prdsinvlem  18204  pwssub  18209  imasgrp  18211  ghmgrp  18219  mulgcl  18241  mulgaddcomlem  18246  mulginvcom  18248  mulginvinv  18249  mulgneg2  18257  subginv  18282  subginvcl  18284  issubg4  18294  grpissubg  18295  isnsg3  18308  subgacs  18309  nmzsubg  18313  eqger  18326  eqglact  18327  eqgcpbl  18330  qusgrp  18331  qusinv  18335  qussub  18336  ghminv  18361  ghmsub  18362  ghmrn  18367  ghmpreima  18376  ghmeql  18377  conjghm  18385  conjnmz  18388  galcan  18430  gacan  18431  gapm  18432  gaorber  18434  gastacl  18435  gastacos  18436  cntzsubg  18463  oppggrp  18481  symgsssg  18591  symgfisg  18592  odinv  18684  sylow2blem1  18741  sylow2blem3  18743  frgpuptf  18892  frgpuplem  18894  ablinvadd  18927  ablsub2inv  18928  ablsub4  18930  ablsubsub4  18936  mulgsubdi  18947  invghm  18951  eqgabl  18952  torsubg  18971  oddvdssubg  18972  cyggeninv  18999  ringnegl  19344  rngnegr  19345  ringmneg1  19346  ringmneg2  19347  ringm2neg  19348  ringsubdi  19349  rngsubdir  19350  dvdsrneg  19404  unitinvcl  19424  unitnegcl  19431  isdrng2  19509  cntzsubr  19565  abvneg  19602  abvsubtri  19603  lmodvnegcl  19672  lmodvneg1  19674  lmodvsneg  19675  lmodsubvs  19687  lmodsubdi  19688  lmodsubdir  19689  lssvsubcl  19712  lssvnegcl  19725  lspsnneg  19775  lmodvsinv  19805  lmodvsinv2  19806  lspexch  19898  lspsolvlem  19911  zrhpsgninv  20278  evpmodpmf1o  20289  dsmmsubg  20436  mplsubglem  20676  mplind  20745  mhpinvcl  20804  cpmatinvcl  21326  chpscmatgsumbin  21453  chpscmatgsummon  21454  tgplacthmeo  22712  tgpconncomp  22722  qustgpopn  22729  tsmsxplem1  22762  tlmtgp  22805  isngp4  23222  ngpinvds  23223  ngpsubcan  23224  nmtri  23236  ngptgp  23246  tngngp3  23266  ncvspi  23765  deg1suble  24712  deg1sub  24713  dchr2sum  25861  dchrisum0re  26101  ogrpinv0le  30770  ogrpsub  30771  ogrpaddltbi  30773  ogrpaddltrbid  30775  ogrpinv0lt  30777  ogrpinvlt  30778  symgfcoeu  30780  symgsubg  30785  archirngz  30872  archiabllem1b  30875  archiabllem2c  30878  orngsqr  30932  eqgvscpbl  30974  qusxpid  30983  linds2eq  30999  madjusmdetlem3  31186  madjusmdetlem4  31187  lflsub  36362  lflnegcl  36370  ldualvsubcl  36451  ldualvsubval  36452  dvhgrp  38402  lcfrlem2  38838  lcdvsubval  38913  mapdpglem30  38997  baerlem3lem1  39002  baerlem5alem1  39003  baerlem5blem1  39004  baerlem5blem2  39007  nelsubginvcld  39420  invginvrid  44766  lincext1  44860  lindslinindimp2lem1  44864  ldepsprlem  44878  ldepspr  44879  lincresunit3lem3  44880  lincresunit3lem1  44885  lincresunit3lem2  44886  lincresunit3  44887
  Copyright terms: Public domain W3C validator