Theorem grpinvcl 19027

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  Basecbs 17258  Grpcgrp 18973  inv_gcminusg 18974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-riota 7404  df-ov 7451  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976  df-minusg 18977

This theorem is referenced by:  grpinvcld  19028  grprinv  19030  grpinvid1  19031  grpinvid2  19032  grplrinv  19036  grplcan  19040  grpasscan1  19041  grpasscan2  19042  grpinvinv  19045  grpinvcnv  19046  grpinvnzcl  19051  grpsubinv  19052  grplmulf1o  19053  grpinvssd  19057  grpinvadd  19058  grpsubf  19059  grpsubrcan  19061  grpinvsub  19062  grpinvval2  19063  grpsubeq0  19066  grpsubadd  19068  grpaddsubass  19070  grpnpcan  19072  dfgrp3  19079  grplactcnv  19083  grpsubpropd2  19086  prdsinvlem  19089  pwssub  19094  imasgrp  19096  ghmgrp  19106  mulgcl  19131  mulgaddcomlem  19137  mulginvcom  19139  mulginvinv  19140  mulgneg2  19148  subginv  19173  subginvcl  19175  issubg4  19185  grpissubg  19186  isnsg3  19200  subgacs  19201  nmzsubg  19205  eqglact  19219  eqgcpbl  19222  qusgrp  19226  qusinv  19230  qussub  19231  eqg0subg  19236  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  19400  symgsssg  19509  symgfisg  19510  odinv  19603  sylow2blem1  19662  sylow2blem3  19664  frgpuptf  19812  frgpuplem  19814  ablinvadd  19849  ablsub2inv  19850  ablsub4  19852  ablsubsub4  19860  mulgsubdi  19871  invghm  19875  eqgabl  19876  torsubg  19896  oddvdssubg  19897  cyggeninv  19925  ringnegl  20325  ringnegr  20326  ringmneg1  20327  ringmneg2  20328  dvdsrneg  20396  unitinvcl  20416  unitnegcl  20423  cntzsubr  20634  isdrng2  20765  abvneg  20849  abvsubtri  20850  lmodvnegcl  20923  lmodvneg1  20925  lmodvsneg  20926  lmodsubvs  20938  lmodsubdi  20939  lmodsubdir  20940  lssvsubcl  20965  lspsnneg  21027  lmodvsinv  21058  lmodvsinv2  21059  lspexch  21154  lspsolvlem  21167  zrhpsgninv  21626  evpmodpmf1o  21637  dsmmsubg  21786  mplsubglem  22042  mplind  22117  cpmatinvcl  22744  chpscmatgsumbin  22871  chpscmatgsummon  22872  tgplacthmeo  24132  tgpconncomp  24142  qustgpopn  24149  tsmsxplem1  24182  tlmtgp  24225  isngp4  24646  ngpinvds  24647  ngpsubcan  24648  nmtri  24660  ngptgp  24670  tngngp3  24698  ncvspi  25209  deg1suble  26166  deg1sub  26167  dchr2sum  27335  dchrisum0re  27575  ogrpinv0le  33065  ogrpsub  33066  ogrpaddltbi  33068  ogrpaddltrbid  33070  ogrpinv0lt  33072  ogrpinvlt  33073  symgfcoeu  33075  symgsubg  33080  archirngz  33169  archiabllem1b  33172  archiabllem2c  33175  orngsqr  33299  eqgvscpbl  33343  qusxpid  33356  linds2eq  33374  quslsm  33398  nsgmgclem  33404  ressply1sub  33560  madjusmdetlem3  33775  madjusmdetlem4  33776  lflsub  39023  lflnegcl  39031  ldualvsubcl  39112  ldualvsubval  39113  dvhgrp  41064  lcfrlem2  41500  lcdvsubval  41575  mapdpglem30  41659  baerlem3lem1  41664  baerlem5alem1  41665  baerlem5blem1  41666  baerlem5blem2  41669  fldhmf1  42047  nelsubginvcld  42451  invginvrid  48092  lincext1  48183  lindslinindimp2lem1  48187  ldepsprlem  48201  ldepspr  48202  lincresunit3lem3  48203  lincresunit3lem1  48208  lincresunit3lem2  48209  lincresunit3  48210