Theorem grpinvcl 18954

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 18953	. 2 ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵)
4	3	ffvelcdmda 7030	1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  Basecbs 17170  Grpcgrp 18900  inv_gcminusg 18901

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 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-riota 7317  df-ov 7363  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903  df-minusg 18904

This theorem is referenced by:  grpinvcld  18955  grprinv  18957  grpinvid1  18958  grpinvid2  18959  grplrinv  18963  grplcan  18967  grpasscan1  18968  grpasscan2  18969  grpinvinv  18972  grpinvcnv  18973  grpinvnzcl  18978  grpsubinv  18979  grplmulf1o  18980  grpinvssd  18984  grpinvadd  18985  grpsubf  18986  grpsubrcan  18988  grpinvsub  18989  grpinvval2  18990  grpsubeq0  18993  grpsubadd  18995  grpaddsubass  18997  grpnpcan  18999  dfgrp3  19006  grplactcnv  19010  grpsubpropd2  19013  prdsinvlem  19016  pwssub  19021  imasgrp  19023  ghmgrp  19033  mulgcl  19058  mulgaddcomlem  19064  mulginvcom  19066  mulginvinv  19067  mulgneg2  19075  subginv  19100  subginvcl  19102  issubg4  19112  grpissubg  19113  isnsg3  19126  subgacs  19127  nmzsubg  19131  eqglact  19145  eqgcpbl  19148  qusgrp  19152  qusinv  19156  qussub  19157  eqg0subg  19162  ghminv  19189  ghmsub  19190  ghmrn  19195  ghmpreima  19204  ghmeql  19205  conjghm  19215  galcan  19270  gacan  19271  gapm  19272  gaorber  19274  gastacl  19275  gastacos  19276  cntzsubg  19305  oppggrp  19323  symgsssg  19433  symgfisg  19434  odinv  19527  sylow2blem1  19586  sylow2blem3  19588  frgpuptf  19736  frgpuplem  19738  ablinvadd  19773  ablsub2inv  19774  ablsub4  19776  ablsubsub4  19784  mulgsubdi  19795  invghm  19799  eqgabl  19800  torsubg  19820  oddvdssubg  19821  cyggeninv  19849  ogrpinv0le  20102  ogrpsub  20103  ogrpaddltbi  20105  ogrpaddltrbid  20107  ogrpinv0lt  20109  ogrpinvlt  20110  ringnegl  20274  ringnegr  20275  ringmneg1  20276  ringmneg2  20277  dvdsrneg  20341  unitinvcl  20361  unitnegcl  20368  cntzsubr  20574  isdrng2  20711  abvneg  20794  abvsubtri  20795  orngsqr  20834  lmodvnegcl  20889  lmodvneg1  20891  lmodvsneg  20892  lmodsubvs  20904  lmodsubdi  20905  lmodsubdir  20906  lssvsubcl  20930  lspsnneg  20992  lmodvsinv  21023  lmodvsinv2  21024  lspexch  21119  lspsolvlem  21132  zrhpsgninv  21575  evpmodpmf1o  21586  dsmmsubg  21733  mplsubglem  21987  mplind  22058  cpmatinvcl  22692  chpscmatgsumbin  22819  chpscmatgsummon  22820  tgplacthmeo  24078  tgpconncomp  24088  qustgpopn  24095  tsmsxplem1  24128  tlmtgp  24171  isngp4  24587  ngpinvds  24588  ngpsubcan  24589  nmtri  24601  ngptgp  24611  tngngp3  24631  ncvspi  25133  deg1suble  26082  deg1sub  26083  dchr2sum  27250  dchrisum0re  27490  symgfcoeu  33158  symgsubg  33163  archirngz  33265  archiabllem1b  33268  archiabllem2c  33271  eqgvscpbl  33425  qusxpid  33438  linds2eq  33456  quslsm  33480  nsgmgclem  33486  ressply1sub  33645  madjusmdetlem3  33989  madjusmdetlem4  33990  lflsub  39527  lflnegcl  39535  ldualvsubcl  39616  ldualvsubval  39617  dvhgrp  41567  lcfrlem2  42003  lcdvsubval  42078  mapdpglem30  42162  baerlem3lem1  42167  baerlem5alem1  42168  baerlem5blem1  42169  baerlem5blem2  42172  fldhmf1  42543  nelsubginvcld  42955  invginvrid  48855  lincext1  48942  lindslinindimp2lem1  48946  ldepsprlem  48960  ldepspr  48961  lincresunit3lem3  48962  lincresunit3lem1  48967  lincresunit3lem2  48968  lincresunit3  48969