Theorem grpinvcl 18901

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6499  Basecbs 17155  Grpcgrp 18847  inv_gcminusg 18848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-riota 7326  df-ov 7372  df-0g 17380  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-grp 18850  df-minusg 18851

This theorem is referenced by:  grpinvcld  18902  grprinv  18904  grpinvid1  18905  grpinvid2  18906  grplrinv  18910  grplcan  18914  grpasscan1  18915  grpasscan2  18916  grpinvinv  18919  grpinvcnv  18920  grpinvnzcl  18925  grpsubinv  18926  grplmulf1o  18927  grpinvssd  18931  grpinvadd  18932  grpsubf  18933  grpsubrcan  18935  grpinvsub  18936  grpinvval2  18937  grpsubeq0  18940  grpsubadd  18942  grpaddsubass  18944  grpnpcan  18946  dfgrp3  18953  grplactcnv  18957  grpsubpropd2  18960  prdsinvlem  18963  pwssub  18968  imasgrp  18970  ghmgrp  18980  mulgcl  19005  mulgaddcomlem  19011  mulginvcom  19013  mulginvinv  19014  mulgneg2  19022  subginv  19047  subginvcl  19049  issubg4  19059  grpissubg  19060  isnsg3  19074  subgacs  19075  nmzsubg  19079  eqglact  19093  eqgcpbl  19096  qusgrp  19100  qusinv  19104  qussub  19105  eqg0subg  19110  ghminv  19137  ghmsub  19138  ghmrn  19143  ghmpreima  19152  ghmeql  19153  conjghm  19163  galcan  19218  gacan  19219  gapm  19220  gaorber  19222  gastacl  19223  gastacos  19224  cntzsubg  19253  oppggrp  19271  symgsssg  19381  symgfisg  19382  odinv  19475  sylow2blem1  19534  sylow2blem3  19536  frgpuptf  19684  frgpuplem  19686  ablinvadd  19721  ablsub2inv  19722  ablsub4  19724  ablsubsub4  19732  mulgsubdi  19743  invghm  19747  eqgabl  19748  torsubg  19768  oddvdssubg  19769  cyggeninv  19797  ogrpinv0le  20050  ogrpsub  20051  ogrpaddltbi  20053  ogrpaddltrbid  20055  ogrpinv0lt  20057  ogrpinvlt  20058  ringnegl  20222  ringnegr  20223  ringmneg1  20224  ringmneg2  20225  dvdsrneg  20290  unitinvcl  20310  unitnegcl  20317  cntzsubr  20526  isdrng2  20663  abvneg  20746  abvsubtri  20747  orngsqr  20786  lmodvnegcl  20841  lmodvneg1  20843  lmodvsneg  20844  lmodsubvs  20856  lmodsubdi  20857  lmodsubdir  20858  lssvsubcl  20882  lspsnneg  20944  lmodvsinv  20975  lmodvsinv2  20976  lspexch  21071  lspsolvlem  21084  zrhpsgninv  21527  evpmodpmf1o  21538  dsmmsubg  21685  mplsubglem  21941  mplind  22010  cpmatinvcl  22637  chpscmatgsumbin  22764  chpscmatgsummon  22765  tgplacthmeo  24023  tgpconncomp  24033  qustgpopn  24040  tsmsxplem1  24073  tlmtgp  24116  isngp4  24533  ngpinvds  24534  ngpsubcan  24535  nmtri  24547  ngptgp  24557  tngngp3  24577  ncvspi  25089  deg1suble  26045  deg1sub  26046  dchr2sum  27217  dchrisum0re  27457  symgfcoeu  33054  symgsubg  33059  archirngz  33158  archiabllem1b  33161  archiabllem2c  33164  eqgvscpbl  33314  qusxpid  33327  linds2eq  33345  quslsm  33369  nsgmgclem  33375  ressply1sub  33532  madjusmdetlem3  33812  madjusmdetlem4  33813  lflsub  39053  lflnegcl  39061  ldualvsubcl  39142  ldualvsubval  39143  dvhgrp  41094  lcfrlem2  41530  lcdvsubval  41605  mapdpglem30  41689  baerlem3lem1  41694  baerlem5alem1  41695  baerlem5blem1  41696  baerlem5blem2  41699  fldhmf1  42071  nelsubginvcld  42477  invginvrid  48348  lincext1  48436  lindslinindimp2lem1  48440  ldepsprlem  48454  ldepspr  48455  lincresunit3lem3  48456  lincresunit3lem1  48461  lincresunit3lem2  48462  lincresunit3  48463