Theorem grpinvcl 18627

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ‘cfv 6433  Basecbs 16912  Grpcgrp 18577  inv_gcminusg 18578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-riota 7232  df-ov 7278  df-0g 17152  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-grp 18580  df-minusg 18581

This theorem is referenced by:  grprinv  18629  grpinvid1  18630  grpinvid2  18631  grplrinv  18633  grplcan  18637  grpasscan1  18638  grpasscan2  18639  grpinvinv  18642  grpinvcnv  18643  grpinvnzcl  18647  grpsubinv  18648  grplmulf1o  18649  grpinvssd  18652  grpinvadd  18653  grpsubf  18654  grpsubrcan  18656  grpinvsub  18657  grpinvval2  18658  grpsubeq0  18661  grpsubadd  18663  grpaddsubass  18665  grpnpcan  18667  dfgrp3  18674  grplactcnv  18678  grpsubpropd2  18681  prdsinvlem  18684  pwssub  18689  imasgrp  18691  ghmgrp  18699  mulgcl  18721  mulgaddcomlem  18726  mulginvcom  18728  mulginvinv  18729  mulgneg2  18737  subginv  18762  subginvcl  18764  issubg4  18774  grpissubg  18775  isnsg3  18788  subgacs  18789  nmzsubg  18793  eqger  18806  eqglact  18807  eqgcpbl  18810  qusgrp  18811  qusinv  18815  qussub  18816  ghminv  18841  ghmsub  18842  ghmrn  18847  ghmpreima  18856  ghmeql  18857  conjghm  18865  conjnmz  18868  galcan  18910  gacan  18911  gapm  18912  gaorber  18914  gastacl  18915  gastacos  18916  cntzsubg  18943  oppggrp  18964  symgsssg  19075  symgfisg  19076  odinv  19168  sylow2blem1  19225  sylow2blem3  19227  frgpuptf  19376  frgpuplem  19378  ablinvadd  19411  ablsub2inv  19412  ablsub4  19414  ablsubsub4  19420  mulgsubdi  19431  invghm  19435  eqgabl  19436  torsubg  19455  oddvdssubg  19456  cyggeninv  19483  ringnegl  19833  rngnegr  19834  ringmneg1  19835  ringmneg2  19836  ringm2neg  19837  ringsubdi  19838  rngsubdir  19839  dvdsrneg  19896  unitinvcl  19916  unitnegcl  19923  isdrng2  20001  cntzsubr  20057  abvneg  20094  abvsubtri  20095  lmodvnegcl  20164  lmodvneg1  20166  lmodvsneg  20167  lmodsubvs  20179  lmodsubdi  20180  lmodsubdir  20181  lssvsubcl  20205  lssvnegcl  20218  lspsnneg  20268  lmodvsinv  20298  lmodvsinv2  20299  lspexch  20391  lspsolvlem  20404  zrhpsgninv  20790  evpmodpmf1o  20801  dsmmsubg  20950  mplsubglem  21205  mplind  21278  mhpinvcl  21342  cpmatinvcl  21866  chpscmatgsumbin  21993  chpscmatgsummon  21994  tgplacthmeo  23254  tgpconncomp  23264  qustgpopn  23271  tsmsxplem1  23304  tlmtgp  23347  isngp4  23768  ngpinvds  23769  ngpsubcan  23770  nmtri  23782  ngptgp  23792  tngngp3  23820  ncvspi  24320  deg1suble  25272  deg1sub  25273  dchr2sum  26421  dchrisum0re  26661  ogrpinv0le  31341  ogrpsub  31342  ogrpaddltbi  31344  ogrpaddltrbid  31346  ogrpinv0lt  31348  ogrpinvlt  31349  symgfcoeu  31351  symgsubg  31356  archirngz  31443  archiabllem1b  31446  archiabllem2c  31449  orngsqr  31503  eqgvscpbl  31550  qusxpid  31559  linds2eq  31575  quslsm  31593  nsgmgclem  31596  madjusmdetlem3  31779  madjusmdetlem4  31780  lflsub  37081  lflnegcl  37089  ldualvsubcl  37170  ldualvsubval  37171  dvhgrp  39121  lcfrlem2  39557  lcdvsubval  39632  mapdpglem30  39716  baerlem3lem1  39721  baerlem5alem1  39722  baerlem5blem1  39723  baerlem5blem2  39726  nelsubginvcld  40220  invginvrid  45703  lincext1  45795  lindslinindimp2lem1  45799  ldepsprlem  45813  ldepspr  45814  lincresunit3lem3  45815  lincresunit3lem1  45820  lincresunit3lem2  45821  lincresunit3  45822