Theorem grpinvcl 18145

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ‘cfv 6350  Basecbs 16477  Grpcgrp 18097  inv_gcminusg 18098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-fv 6358  df-riota 7108  df-ov 7153  df-0g 16709  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-grp 18100  df-minusg 18101

This theorem is referenced by:  grprinv  18147  grpinvid1  18148  grpinvid2  18149  grplrinv  18151  grplcan  18155  grpasscan1  18156  grpasscan2  18157  grpinvinv  18160  grpinvcnv  18161  grpinvnzcl  18165  grpsubinv  18166  grplmulf1o  18167  grpinvssd  18170  grpinvadd  18171  grpsubf  18172  grpsubrcan  18174  grpinvsub  18175  grpinvval2  18176  grpsubeq0  18179  grpsubadd  18181  grpaddsubass  18183  grpnpcan  18185  dfgrp3  18192  grplactcnv  18196  grpsubpropd2  18199  prdsinvlem  18202  pwssub  18207  imasgrp  18209  ghmgrp  18217  mulgcl  18239  mulgaddcomlem  18244  mulginvcom  18246  mulginvinv  18247  mulgneg2  18255  subginv  18280  subginvcl  18282  issubg4  18292  grpissubg  18293  isnsg3  18306  subgacs  18307  nmzsubg  18311  eqger  18324  eqglact  18325  eqgcpbl  18328  qusgrp  18329  qusinv  18333  qussub  18334  ghminv  18359  ghmsub  18360  ghmrn  18365  ghmpreima  18374  ghmeql  18375  conjghm  18383  conjnmz  18386  galcan  18428  gacan  18429  gapm  18430  gaorber  18432  gastacl  18433  gastacos  18434  cntzsubg  18461  oppggrp  18479  symgsssg  18589  symgfisg  18590  odinv  18682  sylow2blem1  18739  sylow2blem3  18741  frgpuptf  18890  frgpuplem  18892  ablinvadd  18924  ablsub2inv  18925  ablsub4  18927  ablsubsub4  18933  mulgsubdi  18944  invghm  18948  eqgabl  18949  torsubg  18968  oddvdssubg  18969  cyggeninv  18996  ringnegl  19338  rngnegr  19339  ringmneg1  19340  ringmneg2  19341  ringm2neg  19342  ringsubdi  19343  rngsubdir  19344  dvdsrneg  19398  unitinvcl  19418  unitnegcl  19425  isdrng2  19506  cntzsubr  19562  abvneg  19599  abvsubtri  19600  lmodvnegcl  19669  lmodvneg1  19671  lmodvsneg  19672  lmodsubvs  19684  lmodsubdi  19685  lmodsubdir  19686  lssvsubcl  19709  lssvnegcl  19722  lspsnneg  19772  lmodvsinv  19802  lmodvsinv2  19803  lspexch  19895  lspsolvlem  19908  mplsubglem  20208  mplind  20276  mhpinvcl  20333  zrhpsgninv  20723  evpmodpmf1o  20734  dsmmsubg  20881  cpmatinvcl  21319  chpscmatgsumbin  21446  chpscmatgsummon  21447  tgplacthmeo  22705  tgpconncomp  22715  qustgpopn  22722  tsmsxplem1  22755  tlmtgp  22798  isngp4  23215  ngpinvds  23216  ngpsubcan  23217  nmtri  23229  ngptgp  23239  tngngp3  23259  ncvspi  23754  deg1suble  24695  deg1sub  24696  dchr2sum  25843  dchrisum0re  26083  ogrpinv0le  30711  ogrpsub  30712  ogrpaddltbi  30714  ogrpaddltrbid  30716  ogrpinv0lt  30718  ogrpinvlt  30719  symgfcoeu  30721  symgsubg  30726  archirngz  30813  archiabllem1b  30816  archiabllem2c  30819  orngsqr  30872  eqgvscpbl  30914  qusxpid  30923  linds2eq  30936  madjusmdetlem3  31089  madjusmdetlem4  31090  lflsub  36197  lflnegcl  36205  ldualvsubcl  36286  ldualvsubval  36287  dvhgrp  38237  lcfrlem2  38673  lcdvsubval  38748  mapdpglem30  38832  baerlem3lem1  38837  baerlem5alem1  38838  baerlem5blem1  38839  baerlem5blem2  38842  nelsubginvcld  39121  invginvrid  44408  lincext1  44502  lindslinindimp2lem1  44506  ldepsprlem  44520  ldepspr  44521  lincresunit3lem3  44522  lincresunit3lem1  44527  lincresunit3lem2  44528  lincresunit3  44529