Theorem grpinvcl 19114

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  Basecbs 17304  Grpcgrp 19060  inv_gcminusg 19061

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-riota 7371  df-ov 7417  df-0g 17529  df-mgm 18733  df-sgrp 18824  df-mnd 18840  df-grp 19063  df-minusg 19064

This theorem is used by:  grpinvcld  19115  grprinv  19117  grpinvid1  19118  grpinvid2  19119  grplrinv  19123  grplcan  19127  grpasscan1  19128  grpasscan2  19129  grpinvinv  19132  grpinvcnv  19133  grpinvnzcl  19137  grpsubinv  19138  grplmulf1o  19139  grpinvssd  19143  grpinvadd  19144  grpsubf  19145  grpsubrcan  19147  grpinvsub  19148  grpinvval2  19149  grpsubeq0  19152  grpsubadd  19154  grpaddsubass  19156  grpnpcan  19158  dfgrp3  19165  grplactcnv  19169  grpsubpropd2  19172  prdsinvlem  19175  pwssub  19180  imasgrp  19182  ghmgrp  19192  mulgcl  19217  mulgaddcomlem  19223  mulginvcom  19225  mulginvinv  19226  mulgneg2  19234  subginv  19259  subginvcl  19261  issubg4  19272  grpissubg  19273  isnsg3  19286  subgacs  19287  nmzsubg  19291  eqglact  19307  eqgcpbl  19310  qusxpid  19311  qusgrp  19317  qusinv  19321  qussub  19322  eqg0subg  19327  ghminv  19353  ghmsub  19354  ghmrn  19359  ghmpreima  19368  ghmeql  19369  conjghm  19379  galcan  19434  gacan  19435  gapm  19436  gaorber  19438  gastacl  19439  gastacos  19440  cntzsubg  19469  oppggrp  19487  symgsssg  19597  symgfisg  19598  odinv  19691  sylow2blem1  19750  sylow2blem3  19752  frgpuptf  19900  frgpuplem  19902  ablinvadd  19937  ablsub2inv  19938  ablsub4  19940  ablsubsub4  19948  mulgsubdi  19959  invghm  19963  eqgabl  19964  torsubg  19984  oddvdssubg  19985  cyggeninv  20013  ogrpinv0le  20266  ogrpsub  20267  ogrpaddltbi  20269  ogrpaddltrbid  20271  ogrpinv0lt  20273  ogrpinvlt  20274  ringnegl  20447  ringnegr  20448  ringmneg1  20449  ringmneg2  20450  dvdsrneg  20514  unitinvcl  20534  unitnegcl  20541  cntzsubr  20771  isdrng2  20909  isdrng3lem1  20917  abvneg  20995  abvsubtri  20996  orngsqr  21035  lmodvnegcl  21090  lmodvneg1  21092  lmodvsneg  21093  lmodsubvs  21105  lmodsubdi  21106  lmodsubdir  21107  lssvsubcl  21131  lspsnneg  21193  lmodvsinv  21223  lmodvsinv2  21224  lspexch  21319  lspsolvlem  21332  zrhpsgninv  21801  evpmodpmf1o  21812  dsmmsubg  21959  mplsubglem  22216  mplind  22289  cpmatinvcl  22945  chpscmatgsumbin  23072  chpscmatgsummon  23073  tgplacthmeo  24332  tgpconncomp  24342  qustgpopn  24349  tsmsxplem1  24382  tlmtgp  24425  isngp4  24841  ngpinvds  24842  ngpsubcan  24843  nmtri  24855  ngptgp  24865  tngngp3  24885  ncvspi  25387  deg1suble  26335  deg1sub  26336  dchr2sum  27512  dchrisum0re  27752  symgfcoeu  33525  symgsubg  33530  archirngz  33632  archiabllem1b  33635  archiabllem2c  33638  eqgvscpbl  33793  linds2eq  33817  quslsm  33837  nsgmgclem  33843  ressply1sub  33983  madjusmdetlem3  34342  madjusmdetlem4  34343  lflsub  39943  lflnegcl  39951  ldualvsubcl  40032  ldualvsubval  40033  dvhgrp  41983  lcfrlem2  42419  lcdvsubval  42494  mapdpglem30  42578  baerlem3lem1  42583  baerlem5alem1  42584  baerlem5blem1  42585  baerlem5blem2  42588  fldhmf1  42959  nelsubginvcld  43387  invginvrid  49300  lincext1  49387  lindslinindimp2lem1  49391  ldepsprlem  49405  ldepspr  49406  lincresunit3lem3  49407  lincresunit3lem1  49412  lincresunit3lem2  49413  lincresunit3  49414