Theorem grpinvcl 19049

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  Basecbs 17264  Grpcgrp 18995  inv_gcminusg 18996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-riota 7367  df-ov 7413  df-0g 17489  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-grp 18998  df-minusg 18999

This theorem is referenced by:  grpinvcld  19050  grprinv  19052  grpinvid1  19053  grpinvid2  19054  grplrinv  19058  grplcan  19062  grpasscan1  19063  grpasscan2  19064  grpinvinv  19067  grpinvcnv  19068  grpinvnzcl  19072  grpsubinv  19073  grplmulf1o  19074  grpinvssd  19078  grpinvadd  19079  grpsubf  19080  grpsubrcan  19082  grpinvsub  19083  grpinvval2  19084  grpsubeq0  19087  grpsubadd  19089  grpaddsubass  19091  grpnpcan  19093  dfgrp3  19100  grplactcnv  19104  grpsubpropd2  19107  prdsinvlem  19110  pwssub  19115  imasgrp  19117  ghmgrp  19127  mulgcl  19152  mulgaddcomlem  19158  mulginvcom  19160  mulginvinv  19161  mulgneg2  19169  subginv  19194  subginvcl  19196  issubg4  19207  grpissubg  19208  isnsg3  19221  subgacs  19222  nmzsubg  19226  eqglact  19242  eqgcpbl  19245  qusxpid  19246  qusgrp  19252  qusinv  19256  qussub  19257  eqg0subg  19262  ghminv  19288  ghmsub  19289  ghmrn  19294  ghmpreima  19303  ghmeql  19304  conjghm  19314  galcan  19369  gacan  19370  gapm  19371  gaorber  19373  gastacl  19374  gastacos  19375  cntzsubg  19404  oppggrp  19422  symgsssg  19532  symgfisg  19533  odinv  19626  sylow2blem1  19685  sylow2blem3  19687  frgpuptf  19835  frgpuplem  19837  ablinvadd  19872  ablsub2inv  19873  ablsub4  19875  ablsubsub4  19883  mulgsubdi  19894  invghm  19898  eqgabl  19899  torsubg  19919  oddvdssubg  19920  cyggeninv  19948  ogrpinv0le  20201  ogrpsub  20202  ogrpaddltbi  20204  ogrpaddltrbid  20206  ogrpinv0lt  20208  ogrpinvlt  20209  ringnegl  20381  ringnegr  20382  ringmneg1  20383  ringmneg2  20384  dvdsrneg  20448  unitinvcl  20468  unitnegcl  20475  cntzsubr  20705  isdrng2  20843  isdrng3lem1  20851  abvneg  20929  abvsubtri  20930  orngsqr  20969  lmodvnegcl  21024  lmodvneg1  21026  lmodvsneg  21027  lmodsubvs  21039  lmodsubdi  21040  lmodsubdir  21041  lssvsubcl  21065  lspsnneg  21127  lmodvsinv  21157  lmodvsinv2  21158  lspexch  21253  lspsolvlem  21266  zrhpsgninv  21735  evpmodpmf1o  21746  dsmmsubg  21893  mplsubglem  22148  mplind  22221  cpmatinvcl  22874  chpscmatgsumbin  23001  chpscmatgsummon  23002  tgplacthmeo  24260  tgpconncomp  24270  qustgpopn  24277  tsmsxplem1  24310  tlmtgp  24353  isngp4  24769  ngpinvds  24770  ngpsubcan  24771  nmtri  24783  ngptgp  24793  tngngp3  24813  ncvspi  25315  deg1suble  26264  deg1sub  26265  dchr2sum  27437  dchrisum0re  27677  symgfcoeu  33402  symgsubg  33407  archirngz  33509  archiabllem1b  33512  archiabllem2c  33515  eqgvscpbl  33670  linds2eq  33694  quslsm  33714  nsgmgclem  33720  ressply1sub  33860  madjusmdetlem3  34219  madjusmdetlem4  34220  lflsub  39861  lflnegcl  39869  ldualvsubcl  39950  ldualvsubval  39951  dvhgrp  41901  lcfrlem2  42337  lcdvsubval  42412  mapdpglem30  42496  baerlem3lem1  42501  baerlem5alem1  42502  baerlem5blem1  42503  baerlem5blem2  42506  fldhmf1  42877  nelsubginvcld  43290  invginvrid  49167  lincext1  49254  lindslinindimp2lem1  49258  ldepsprlem  49272  ldepspr  49273  lincresunit3lem3  49274  lincresunit3lem1  49279  lincresunit3lem2  49280  lincresunit3  49281