Theorem grpinvcl 18915

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ‘cfv 6490  Basecbs 17134  Grpcgrp 18861  inv_gcminusg 18862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-riota 7313  df-ov 7359  df-0g 17359  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-grp 18864  df-minusg 18865

This theorem is referenced by:  grpinvcld  18916  grprinv  18918  grpinvid1  18919  grpinvid2  18920  grplrinv  18924  grplcan  18928  grpasscan1  18929  grpasscan2  18930  grpinvinv  18933  grpinvcnv  18934  grpinvnzcl  18939  grpsubinv  18940  grplmulf1o  18941  grpinvssd  18945  grpinvadd  18946  grpsubf  18947  grpsubrcan  18949  grpinvsub  18950  grpinvval2  18951  grpsubeq0  18954  grpsubadd  18956  grpaddsubass  18958  grpnpcan  18960  dfgrp3  18967  grplactcnv  18971  grpsubpropd2  18974  prdsinvlem  18977  pwssub  18982  imasgrp  18984  ghmgrp  18994  mulgcl  19019  mulgaddcomlem  19025  mulginvcom  19027  mulginvinv  19028  mulgneg2  19036  subginv  19061  subginvcl  19063  issubg4  19073  grpissubg  19074  isnsg3  19087  subgacs  19088  nmzsubg  19092  eqglact  19106  eqgcpbl  19109  qusgrp  19113  qusinv  19117  qussub  19118  eqg0subg  19123  ghminv  19150  ghmsub  19151  ghmrn  19156  ghmpreima  19165  ghmeql  19166  conjghm  19176  galcan  19231  gacan  19232  gapm  19233  gaorber  19235  gastacl  19236  gastacos  19237  cntzsubg  19266  oppggrp  19284  symgsssg  19394  symgfisg  19395  odinv  19488  sylow2blem1  19547  sylow2blem3  19549  frgpuptf  19697  frgpuplem  19699  ablinvadd  19734  ablsub2inv  19735  ablsub4  19737  ablsubsub4  19745  mulgsubdi  19756  invghm  19760  eqgabl  19761  torsubg  19781  oddvdssubg  19782  cyggeninv  19810  ogrpinv0le  20063  ogrpsub  20064  ogrpaddltbi  20066  ogrpaddltrbid  20068  ogrpinv0lt  20070  ogrpinvlt  20071  ringnegl  20235  ringnegr  20236  ringmneg1  20237  ringmneg2  20238  dvdsrneg  20304  unitinvcl  20324  unitnegcl  20331  cntzsubr  20537  isdrng2  20674  abvneg  20757  abvsubtri  20758  orngsqr  20797  lmodvnegcl  20852  lmodvneg1  20854  lmodvsneg  20855  lmodsubvs  20867  lmodsubdi  20868  lmodsubdir  20869  lssvsubcl  20893  lspsnneg  20955  lmodvsinv  20986  lmodvsinv2  20987  lspexch  21082  lspsolvlem  21095  zrhpsgninv  21538  evpmodpmf1o  21549  dsmmsubg  21696  mplsubglem  21952  mplind  22023  cpmatinvcl  22659  chpscmatgsumbin  22786  chpscmatgsummon  22787  tgplacthmeo  24045  tgpconncomp  24055  qustgpopn  24062  tsmsxplem1  24095  tlmtgp  24138  isngp4  24554  ngpinvds  24555  ngpsubcan  24556  nmtri  24568  ngptgp  24578  tngngp3  24598  ncvspi  25110  deg1suble  26066  deg1sub  26067  dchr2sum  27238  dchrisum0re  27478  symgfcoeu  33113  symgsubg  33118  archirngz  33220  archiabllem1b  33223  archiabllem2c  33226  eqgvscpbl  33380  qusxpid  33393  linds2eq  33411  quslsm  33435  nsgmgclem  33441  ressply1sub  33600  madjusmdetlem3  33935  madjusmdetlem4  33936  lflsub  39266  lflnegcl  39274  ldualvsubcl  39355  ldualvsubval  39356  dvhgrp  41306  lcfrlem2  41742  lcdvsubval  41817  mapdpglem30  41901  baerlem3lem1  41906  baerlem5alem1  41907  baerlem5blem1  41908  baerlem5blem2  41911  fldhmf1  42283  nelsubginvcld  42693  invginvrid  48555  lincext1  48642  lindslinindimp2lem1  48646  ldepsprlem  48660  ldepspr  48661  lincresunit3lem3  48662  lincresunit3lem1  48667  lincresunit3lem2  48668  lincresunit3  48669