Theorem grpinvcl 18134

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ‘cfv 6341  Basecbs 16466  Grpcgrp 18086  inv_gcminusg 18087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  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 3488  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-fv 6349  df-riota 7100  df-ov 7145  df-0g 16698  df-mgm 17835  df-sgrp 17884  df-mnd 17895  df-grp 18089  df-minusg 18090

This theorem is referenced by:  grprinv  18136  grpinvid1  18137  grpinvid2  18138  grplrinv  18140  grplcan  18144  grpasscan1  18145  grpasscan2  18146  grpinvinv  18149  grpinvcnv  18150  grpinvnzcl  18154  grpsubinv  18155  grplmulf1o  18156  grpinvssd  18159  grpinvadd  18160  grpsubf  18161  grpsubrcan  18163  grpinvsub  18164  grpinvval2  18165  grpsubeq0  18168  grpsubadd  18170  grpaddsubass  18172  grpnpcan  18174  dfgrp3  18181  grplactcnv  18185  grpsubpropd2  18188  prdsinvlem  18191  pwssub  18196  imasgrp  18198  ghmgrp  18206  mulgcl  18228  mulgaddcomlem  18233  mulginvcom  18235  mulginvinv  18236  mulgneg2  18244  subginv  18269  subginvcl  18271  issubg4  18281  grpissubg  18282  isnsg3  18295  subgacs  18296  nmzsubg  18300  eqger  18313  eqglact  18314  eqgcpbl  18317  qusgrp  18318  qusinv  18322  qussub  18323  ghminv  18348  ghmsub  18349  ghmrn  18354  ghmpreima  18363  ghmeql  18364  conjghm  18372  conjnmz  18375  galcan  18417  gacan  18418  gapm  18419  gaorber  18421  gastacl  18422  gastacos  18423  cntzsubg  18450  oppggrp  18468  symgsssg  18578  symgfisg  18579  odinv  18671  sylow2blem1  18728  sylow2blem3  18730  frgpuptf  18879  frgpuplem  18881  ablinvadd  18913  ablsub2inv  18914  ablsub4  18916  ablsubsub4  18922  mulgsubdi  18933  invghm  18937  eqgabl  18938  torsubg  18957  oddvdssubg  18958  cyggeninv  18985  ringnegl  19327  rngnegr  19328  ringmneg1  19329  ringmneg2  19330  ringm2neg  19331  ringsubdi  19332  rngsubdir  19333  dvdsrneg  19387  unitinvcl  19407  unitnegcl  19414  isdrng2  19495  cntzsubr  19551  abvneg  19588  abvsubtri  19589  lmodvnegcl  19658  lmodvneg1  19660  lmodvsneg  19661  lmodsubvs  19673  lmodsubdi  19674  lmodsubdir  19675  lssvsubcl  19698  lssvnegcl  19711  lspsnneg  19761  lmodvsinv  19791  lmodvsinv2  19792  lspexch  19884  lspsolvlem  19897  mplsubglem  20197  mplind  20265  mhpinvcl  20322  zrhpsgninv  20712  evpmodpmf1o  20723  dsmmsubg  20870  cpmatinvcl  21308  chpscmatgsumbin  21435  chpscmatgsummon  21436  tgplacthmeo  22694  tgpconncomp  22704  qustgpopn  22711  tsmsxplem1  22744  tlmtgp  22787  isngp4  23204  ngpinvds  23205  ngpsubcan  23206  nmtri  23218  ngptgp  23228  tngngp3  23248  ncvspi  23743  deg1suble  24687  deg1sub  24688  dchr2sum  25835  dchrisum0re  26075  ogrpinv0le  30723  ogrpsub  30724  ogrpaddltbi  30726  ogrpaddltrbid  30728  ogrpinv0lt  30730  ogrpinvlt  30731  symgfcoeu  30733  symgsubg  30738  archirngz  30825  archiabllem1b  30828  archiabllem2c  30831  orngsqr  30884  eqgvscpbl  30926  qusxpid  30935  linds2eq  30949  madjusmdetlem3  31104  madjusmdetlem4  31105  lflsub  36235  lflnegcl  36243  ldualvsubcl  36324  ldualvsubval  36325  dvhgrp  38275  lcfrlem2  38711  lcdvsubval  38786  mapdpglem30  38870  baerlem3lem1  38875  baerlem5alem1  38876  baerlem5blem1  38877  baerlem5blem2  38880  nelsubginvcld  39203  invginvrid  44500  lincext1  44594  lindslinindimp2lem1  44598  ldepsprlem  44612  ldepspr  44613  lincresunit3lem3  44614  lincresunit3lem1  44619  lincresunit3lem2  44620  lincresunit3  44621