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

Theorem grpinvcl 18935
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 18934 . 2 (𝐺 ∈ Grp → 𝑁:𝐵𝐵)
43ffvelcdmda 7088 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1534  wcel 2099  cfv 6542  Basecbs 17171  Grpcgrp 18881  invgcminusg 18882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-riota 7370  df-ov 7417  df-0g 17414  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-grp 18884  df-minusg 18885
This theorem is referenced by:  grpinvcld  18936  grprinv  18938  grpinvid1  18939  grpinvid2  18940  grplrinv  18944  grplcan  18948  grpasscan1  18949  grpasscan2  18950  grpinvinv  18953  grpinvcnv  18954  grpinvnzcl  18958  grpsubinv  18959  grplmulf1o  18960  grpinvssd  18964  grpinvadd  18965  grpsubf  18966  grpsubrcan  18968  grpinvsub  18969  grpinvval2  18970  grpsubeq0  18973  grpsubadd  18975  grpaddsubass  18977  grpnpcan  18979  dfgrp3  18986  grplactcnv  18990  grpsubpropd2  18993  prdsinvlem  18996  pwssub  19001  imasgrp  19003  ghmgrp  19013  mulgcl  19037  mulgaddcomlem  19043  mulginvcom  19045  mulginvinv  19046  mulgneg2  19054  subginv  19079  subginvcl  19081  issubg4  19091  grpissubg  19092  isnsg3  19106  subgacs  19107  nmzsubg  19111  eqglact  19125  eqgcpbl  19128  qusgrp  19132  qusinv  19136  qussub  19137  eqg0subg  19142  ghminv  19168  ghmsub  19169  ghmrn  19174  ghmpreima  19183  ghmeql  19184  conjghm  19194  conjnmz  19197  galcan  19246  gacan  19247  gapm  19248  gaorber  19250  gastacl  19251  gastacos  19252  cntzsubg  19281  oppggrp  19302  symgsssg  19413  symgfisg  19414  odinv  19507  sylow2blem1  19566  sylow2blem3  19568  frgpuptf  19716  frgpuplem  19718  ablinvadd  19753  ablsub2inv  19754  ablsub4  19756  ablsubsub4  19764  mulgsubdi  19775  invghm  19779  eqgabl  19780  torsubg  19800  oddvdssubg  19801  cyggeninv  19829  ringnegl  20227  ringnegr  20228  ringmneg1  20229  ringmneg2  20230  dvdsrneg  20298  unitinvcl  20318  unitnegcl  20325  cntzsubr  20534  isdrng2  20627  abvneg  20703  abvsubtri  20704  lmodvnegcl  20775  lmodvneg1  20777  lmodvsneg  20778  lmodsubvs  20790  lmodsubdi  20791  lmodsubdir  20792  lssvsubcl  20817  lspsnneg  20879  lmodvsinv  20910  lmodvsinv2  20911  lspexch  21006  lspsolvlem  21019  zrhpsgninv  21504  evpmodpmf1o  21515  dsmmsubg  21664  mplsubglem  21928  mplind  22001  mhpinvcl  22063  cpmatinvcl  22606  chpscmatgsumbin  22733  chpscmatgsummon  22734  tgplacthmeo  23994  tgpconncomp  24004  qustgpopn  24011  tsmsxplem1  24044  tlmtgp  24087  isngp4  24508  ngpinvds  24509  ngpsubcan  24510  nmtri  24522  ngptgp  24532  tngngp3  24560  ncvspi  25071  deg1suble  26030  deg1sub  26031  dchr2sum  27193  dchrisum0re  27433  ogrpinv0le  32773  ogrpsub  32774  ogrpaddltbi  32776  ogrpaddltrbid  32778  ogrpinv0lt  32780  ogrpinvlt  32781  symgfcoeu  32783  symgsubg  32788  archirngz  32875  archiabllem1b  32878  archiabllem2c  32881  orngsqr  32959  eqgvscpbl  33002  qusxpid  33015  linds2eq  33036  quslsm  33055  nsgmgclem  33061  ressply1sub  33181  madjusmdetlem3  33366  madjusmdetlem4  33367  lflsub  38476  lflnegcl  38484  ldualvsubcl  38565  ldualvsubval  38566  dvhgrp  40517  lcfrlem2  40953  lcdvsubval  41028  mapdpglem30  41112  baerlem3lem1  41117  baerlem5alem1  41118  baerlem5blem1  41119  baerlem5blem2  41122  fldhmf1  41498  nelsubginvcld  41656  invginvrid  47354  lincext1  47445  lindslinindimp2lem1  47449  ldepsprlem  47463  ldepspr  47464  lincresunit3lem3  47465  lincresunit3lem1  47470  lincresunit3lem2  47471  lincresunit3  47472
  Copyright terms: Public domain W3C validator