Theorem grpinvcl 19029

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

Step	Hyp	Ref	Expression
1		grpinvcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
2		grpinvcl.n	. . 3 ⊢ 𝑁 = (invg‘𝐺)
3	1, 2	grpinvf 19028	. 2 ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵)
4	3	ffvelcdmda 7065	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ‘cfv 6521  Basecbs 17245  Grpcgrp 18975  inv_gcminusg 18976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-riota 7353  df-ov 7399  df-0g 17470  df-mgm 18674  df-sgrp 18753  df-mnd 18769  df-grp 18978  df-minusg 18979

This theorem is referenced by:  grpinvcld  19030  grprinv  19032  grpinvid1  19033  grpinvid2  19034  grplrinv  19038  grplcan  19042  grpasscan1  19043  grpasscan2  19044  grpinvinv  19047  grpinvcnv  19048  grpinvnzcl  19053  grpsubinv  19054  grplmulf1o  19055  grpinvssd  19059  grpinvadd  19060  grpsubf  19061  grpsubrcan  19063  grpinvsub  19064  grpinvval2  19065  grpsubeq0  19068  grpsubadd  19070  grpaddsubass  19072  grpnpcan  19074  dfgrp3  19081  grplactcnv  19085  grpsubpropd2  19088  prdsinvlem  19091  pwssub  19096  imasgrp  19098  ghmgrp  19108  mulgcl  19133  mulgaddcomlem  19139  mulginvcom  19141  mulginvinv  19142  mulgneg2  19150  subginv  19175  subginvcl  19177  issubg4  19187  grpissubg  19188  isnsg3  19201  subgacs  19202  nmzsubg  19206  eqglact  19220  eqgcpbl  19223  qusgrp  19227  qusinv  19231  qussub  19232  eqg0subg  19237  ghminv  19263  ghmsub  19264  ghmrn  19269  ghmpreima  19278  ghmeql  19279  conjghm  19289  galcan  19344  gacan  19345  gapm  19346  gaorber  19348  gastacl  19349  gastacos  19350  cntzsubg  19379  oppggrp  19397  symgsssg  19507  symgfisg  19508  odinv  19601  sylow2blem1  19660  sylow2blem3  19662  frgpuptf  19810  frgpuplem  19812  ablinvadd  19847  ablsub2inv  19848  ablsub4  19850  ablsubsub4  19858  mulgsubdi  19869  invghm  19873  eqgabl  19874  torsubg  19894  oddvdssubg  19895  cyggeninv  19923  ogrpinv0le  20176  ogrpsub  20177  ogrpaddltbi  20179  ogrpaddltrbid  20181  ogrpinv0lt  20183  ogrpinvlt  20184  ringnegl  20352  ringnegr  20353  ringmneg1  20354  ringmneg2  20355  dvdsrneg  20419  unitinvcl  20439  unitnegcl  20446  cntzsubr  20656  isdrng2  20793  abvneg  20875  abvsubtri  20876  orngsqr  20915  lmodvnegcl  20970  lmodvneg1  20972  lmodvsneg  20973  lmodsubvs  20985  lmodsubdi  20986  lmodsubdir  20987  lssvsubcl  21011  lspsnneg  21073  lmodvsinv  21103  lmodvsinv2  21104  lspexch  21199  lspsolvlem  21212  zrhpsgninv  21637  evpmodpmf1o  21648  dsmmsubg  21795  mplsubglem  22050  mplind  22123  cpmatinvcl  22777  chpscmatgsumbin  22904  chpscmatgsummon  22905  tgplacthmeo  24163  tgpconncomp  24173  qustgpopn  24180  tsmsxplem1  24213  tlmtgp  24256  isngp4  24672  ngpinvds  24673  ngpsubcan  24674  nmtri  24686  ngptgp  24696  tngngp3  24716  ncvspi  25218  deg1suble  26167  deg1sub  26168  dchr2sum  27337  dchrisum0re  27577  symgfcoeu  33262  symgsubg  33267  archirngz  33369  archiabllem1b  33372  archiabllem2c  33375  eqgvscpbl  33536  qusxpid  33549  linds2eq  33567  quslsm  33591  nsgmgclem  33597  ressply1sub  33766  madjusmdetlem3  34126  madjusmdetlem4  34127  lflsub  39691  lflnegcl  39699  ldualvsubcl  39780  ldualvsubval  39781  dvhgrp  41731  lcfrlem2  42167  lcdvsubval  42242  mapdpglem30  42326  baerlem3lem1  42331  baerlem5alem1  42332  baerlem5blem1  42333  baerlem5blem2  42336  fldhmf1  42707  nelsubginvcld  43118  invginvrid  48989  lincext1  49076  lindslinindimp2lem1  49080  ldepsprlem  49094  ldepspr  49095  lincresunit3lem3  49096  lincresunit3lem1  49101  lincresunit3lem2  49102  lincresunit3  49103