Theorem grpinvcl 18847

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ‘cfv 6532  Basecbs 17126  Grpcgrp 18794  inv_gcminusg 18795

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-fv 6540  df-riota 7349  df-ov 7396  df-0g 17369  df-mgm 18543  df-sgrp 18592  df-mnd 18603  df-grp 18797  df-minusg 18798

This theorem is referenced by:  grpinvcld  18848  grprinv  18850  grpinvid1  18851  grpinvid2  18852  grplrinv  18855  grplcan  18859  grpasscan1  18860  grpasscan2  18861  grpinvinv  18864  grpinvcnv  18865  grpinvnzcl  18869  grpsubinv  18870  grplmulf1o  18871  grpinvssd  18874  grpinvadd  18875  grpsubf  18876  grpsubrcan  18878  grpinvsub  18879  grpinvval2  18880  grpsubeq0  18883  grpsubadd  18885  grpaddsubass  18887  grpnpcan  18889  dfgrp3  18896  grplactcnv  18900  grpsubpropd2  18903  prdsinvlem  18906  pwssub  18911  imasgrp  18913  ghmgrp  18921  mulgcl  18943  mulgaddcomlem  18949  mulginvcom  18951  mulginvinv  18952  mulgneg2  18960  subginv  18985  subginvcl  18987  issubg4  18997  grpissubg  18998  isnsg3  19012  subgacs  19013  nmzsubg  19017  eqglact  19031  eqgcpbl  19034  qusgrp  19035  qusinv  19039  qussub  19040  ghminv  19065  ghmsub  19066  ghmrn  19071  ghmpreima  19080  ghmeql  19081  conjghm  19089  conjnmz  19092  galcan  19134  gacan  19135  gapm  19136  gaorber  19138  gastacl  19139  gastacos  19140  cntzsubg  19167  oppggrp  19188  symgsssg  19299  symgfisg  19300  odinv  19393  sylow2blem1  19452  sylow2blem3  19454  frgpuptf  19602  frgpuplem  19604  ablinvadd  19638  ablsub2inv  19639  ablsub4  19641  ablsubsub4  19647  mulgsubdi  19658  invghm  19662  eqgabl  19663  torsubg  19682  oddvdssubg  19683  cyggeninv  19710  ringnegl  20071  ringnegr  20072  ringmneg1  20073  ringmneg2  20074  ringm2neg  20075  ringsubdi  20076  ringsubdir  20077  dvdsrneg  20136  unitinvcl  20156  unitnegcl  20163  isdrng2  20278  cntzsubr  20347  abvneg  20391  abvsubtri  20392  lmodvnegcl  20462  lmodvneg1  20464  lmodvsneg  20465  lmodsubvs  20477  lmodsubdi  20478  lmodsubdir  20479  lssvsubcl  20503  lssvnegcl  20516  lspsnneg  20566  lmodvsinv  20596  lmodvsinv2  20597  lspexch  20691  lspsolvlem  20704  zrhpsgninv  21071  evpmodpmf1o  21082  dsmmsubg  21231  mplsubglem  21487  mplind  21560  mhpinvcl  21624  cpmatinvcl  22148  chpscmatgsumbin  22275  chpscmatgsummon  22276  tgplacthmeo  23536  tgpconncomp  23546  qustgpopn  23553  tsmsxplem1  23586  tlmtgp  23629  isngp4  24050  ngpinvds  24051  ngpsubcan  24052  nmtri  24064  ngptgp  24074  tngngp3  24102  ncvspi  24602  deg1suble  25554  deg1sub  25555  dchr2sum  26703  dchrisum0re  26943  ogrpinv0le  32104  ogrpsub  32105  ogrpaddltbi  32107  ogrpaddltrbid  32109  ogrpinv0lt  32111  ogrpinvlt  32112  symgfcoeu  32114  symgsubg  32119  archirngz  32206  archiabllem1b  32209  archiabllem2c  32212  orngsqr  32284  eqgvscpbl  32327  qusxpid  32337  linds2eq  32355  quslsm  32374  nsgmgclem  32378  ressply1sub  32497  madjusmdetlem3  32638  madjusmdetlem4  32639  lflsub  37740  lflnegcl  37748  ldualvsubcl  37829  ldualvsubval  37830  dvhgrp  39781  lcfrlem2  40217  lcdvsubval  40292  mapdpglem30  40376  baerlem3lem1  40381  baerlem5alem1  40382  baerlem5blem1  40383  baerlem5blem2  40386  fldhmf1  40758  nelsubginvcld  40875  invginvrid  46689  lincext1  46781  lindslinindimp2lem1  46785  ldepsprlem  46799  ldepspr  46800  lincresunit3lem3  46801  lincresunit3lem1  46806  lincresunit3lem2  46807  lincresunit3  46808