Theorem grpinvcl 18369

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ‘cfv 6358  Basecbs 16666  Grpcgrp 18319  inv_gcminusg 18320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-fv 6366  df-riota 7148  df-ov 7194  df-0g 16900  df-mgm 18068  df-sgrp 18117  df-mnd 18128  df-grp 18322  df-minusg 18323

This theorem is referenced by:  grprinv  18371  grpinvid1  18372  grpinvid2  18373  grplrinv  18375  grplcan  18379  grpasscan1  18380  grpasscan2  18381  grpinvinv  18384  grpinvcnv  18385  grpinvnzcl  18389  grpsubinv  18390  grplmulf1o  18391  grpinvssd  18394  grpinvadd  18395  grpsubf  18396  grpsubrcan  18398  grpinvsub  18399  grpinvval2  18400  grpsubeq0  18403  grpsubadd  18405  grpaddsubass  18407  grpnpcan  18409  dfgrp3  18416  grplactcnv  18420  grpsubpropd2  18423  prdsinvlem  18426  pwssub  18431  imasgrp  18433  ghmgrp  18441  mulgcl  18463  mulgaddcomlem  18468  mulginvcom  18470  mulginvinv  18471  mulgneg2  18479  subginv  18504  subginvcl  18506  issubg4  18516  grpissubg  18517  isnsg3  18530  subgacs  18531  nmzsubg  18535  eqger  18548  eqglact  18549  eqgcpbl  18552  qusgrp  18553  qusinv  18557  qussub  18558  ghminv  18583  ghmsub  18584  ghmrn  18589  ghmpreima  18598  ghmeql  18599  conjghm  18607  conjnmz  18610  galcan  18652  gacan  18653  gapm  18654  gaorber  18656  gastacl  18657  gastacos  18658  cntzsubg  18685  oppggrp  18703  symgsssg  18813  symgfisg  18814  odinv  18906  sylow2blem1  18963  sylow2blem3  18965  frgpuptf  19114  frgpuplem  19116  ablinvadd  19149  ablsub2inv  19150  ablsub4  19152  ablsubsub4  19158  mulgsubdi  19169  invghm  19173  eqgabl  19174  torsubg  19193  oddvdssubg  19194  cyggeninv  19221  ringnegl  19566  rngnegr  19567  ringmneg1  19568  ringmneg2  19569  ringm2neg  19570  ringsubdi  19571  rngsubdir  19572  dvdsrneg  19626  unitinvcl  19646  unitnegcl  19653  isdrng2  19731  cntzsubr  19787  abvneg  19824  abvsubtri  19825  lmodvnegcl  19894  lmodvneg1  19896  lmodvsneg  19897  lmodsubvs  19909  lmodsubdi  19910  lmodsubdir  19911  lssvsubcl  19934  lssvnegcl  19947  lspsnneg  19997  lmodvsinv  20027  lmodvsinv2  20028  lspexch  20120  lspsolvlem  20133  zrhpsgninv  20501  evpmodpmf1o  20512  dsmmsubg  20659  mplsubglem  20915  mplind  20982  mhpinvcl  21046  cpmatinvcl  21568  chpscmatgsumbin  21695  chpscmatgsummon  21696  tgplacthmeo  22954  tgpconncomp  22964  qustgpopn  22971  tsmsxplem1  23004  tlmtgp  23047  isngp4  23464  ngpinvds  23465  ngpsubcan  23466  nmtri  23478  ngptgp  23488  tngngp3  23508  ncvspi  24007  deg1suble  24959  deg1sub  24960  dchr2sum  26108  dchrisum0re  26348  ogrpinv0le  31014  ogrpsub  31015  ogrpaddltbi  31017  ogrpaddltrbid  31019  ogrpinv0lt  31021  ogrpinvlt  31022  symgfcoeu  31024  symgsubg  31029  archirngz  31116  archiabllem1b  31119  archiabllem2c  31122  orngsqr  31176  eqgvscpbl  31218  qusxpid  31227  linds2eq  31243  quslsm  31261  nsgmgclem  31264  madjusmdetlem3  31447  madjusmdetlem4  31448  lflsub  36767  lflnegcl  36775  ldualvsubcl  36856  ldualvsubval  36857  dvhgrp  38807  lcfrlem2  39243  lcdvsubval  39318  mapdpglem30  39402  baerlem3lem1  39407  baerlem5alem1  39408  baerlem5blem1  39409  baerlem5blem2  39412  nelsubginvcld  39874  invginvrid  45319  lincext1  45411  lindslinindimp2lem1  45415  ldepsprlem  45429  ldepspr  45430  lincresunit3lem3  45431  lincresunit3lem1  45436  lincresunit3lem2  45437  lincresunit3  45438