Theorem grpinvcl 17913

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ‘cfv 6230  Basecbs 16317  Grpcgrp 17866  inv_gcminusg 17867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-fv 6238  df-riota 6982  df-ov 7024  df-0g 16549  df-mgm 17686  df-sgrp 17728  df-mnd 17739  df-grp 17869  df-minusg 17870

This theorem is referenced by:  grprinv  17915  grpinvid1  17916  grpinvid2  17917  grplrinv  17919  grplcan  17923  grpasscan1  17924  grpasscan2  17925  grpinvinv  17928  grpinvcnv  17929  grpinvnzcl  17933  grpsubinv  17934  grplmulf1o  17935  grpinvssd  17938  grpinvadd  17939  grpsubf  17940  grpsubrcan  17942  grpinvsub  17943  grpinvval2  17944  grpsubeq0  17947  grpsubadd  17949  grpaddsubass  17951  grpnpcan  17953  dfgrp3  17960  grplactcnv  17964  grpsubpropd2  17967  prdsinvlem  17970  pwssub  17975  imasgrp  17977  ghmgrp  17985  mulgcl  18005  mulgaddcomlem  18009  mulginvcom  18011  mulginvinv  18012  mulgneg2  18020  subginv  18045  subginvcl  18047  issubg4  18057  grpissubg  18058  isnsg3  18072  subgacs  18073  nmzsubg  18079  eqger  18088  eqglact  18089  eqgcpbl  18092  qusgrp  18093  qusinv  18097  qussub  18098  ghminv  18111  ghmsub  18112  ghmrn  18117  ghmpreima  18126  ghmeql  18127  conjghm  18135  conjnmz  18138  galcan  18180  gacan  18181  gapm  18182  gaorber  18184  gastacl  18185  gastacos  18186  cntzsubg  18213  oppggrp  18231  symgsssg  18331  symgfisg  18332  odinv  18423  sylow2blem1  18480  sylow2blem3  18482  frgpuptf  18628  frgpuplem  18630  ablinvadd  18660  ablsub2inv  18661  ablsub4  18663  ablsubsub4  18669  mulgsubdi  18680  invghm  18684  eqgabl  18685  torsubg  18702  oddvdssubg  18703  cyggeninv  18730  ringnegl  19039  rngnegr  19040  ringmneg1  19041  ringmneg2  19042  ringm2neg  19043  ringsubdi  19044  rngsubdir  19045  dvdsrneg  19099  unitinvcl  19119  unitnegcl  19126  isdrng2  19207  cntzsubr  19263  abvneg  19300  abvsubtri  19301  lmodvnegcl  19370  lmodvneg1  19372  lmodvsneg  19373  lmodsubvs  19385  lmodsubdi  19386  lmodsubdir  19387  lssvsubcl  19410  lssvnegcl  19423  lspsnneg  19473  lmodvsinv  19503  lmodvsinv2  19504  lspexch  19596  lspsolvlem  19609  mplsubglem  19907  mplind  19974  mhpinvcl  20027  zrhpsgninv  20416  evpmodpmf1o  20427  dsmmsubg  20574  cpmatinvcl  21014  chpscmatgsumbin  21141  chpscmatgsummon  21142  tgplacthmeo  22400  tgpconncomp  22409  qustgpopn  22416  tsmsxplem1  22449  tlmtgp  22492  isngp4  22909  ngpinvds  22910  ngpsubcan  22911  nmtri  22923  ngptgp  22933  tngngp3  22953  ncvspi  23448  deg1suble  24389  deg1sub  24390  dchr2sum  25536  dchrisum0re  25776  ogrpinv0le  30381  ogrpsub  30382  ogrpaddltbi  30384  ogrpaddltrbid  30386  ogrpinv0lt  30388  ogrpinvlt  30389  symgfcoeu  30390  symgsubg  30395  archirngz  30461  archiabllem1b  30464  archiabllem2c  30467  orngsqr  30536  eqgvscpbl  30578  linds2eq  30592  madjusmdetlem3  30714  madjusmdetlem4  30715  lflsub  35759  lflnegcl  35767  ldualvsubcl  35848  ldualvsubval  35849  dvhgrp  37799  lcfrlem2  38235  lcdvsubval  38310  mapdpglem30  38394  baerlem3lem1  38399  baerlem5alem1  38400  baerlem5blem1  38401  baerlem5blem2  38404  nelsubginvcld  38683  invginvrid  43921  lincext1  44015  lindslinindimp2lem1  44019  ldepsprlem  44033  ldepspr  44034  lincresunit3lem3  44035  lincresunit3lem1  44040  lincresunit3lem2  44041  lincresunit3  44042