Theorem grpinvcl 19100

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  Basecbs 17293  Grpcgrp 19046  inv_gcminusg 19047

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-riota 7376  df-ov 7422  df-0g 17518  df-mgm 18722  df-sgrp 18811  df-mnd 18827  df-grp 19049  df-minusg 19050

This theorem is used by:  grpinvcld  19101  grprinv  19103  grpinvid1  19104  grpinvid2  19105  grplrinv  19109  grplcan  19113  grpasscan1  19114  grpasscan2  19115  grpinvinv  19118  grpinvcnv  19119  grpinvnzcl  19123  grpsubinv  19124  grplmulf1o  19125  grpinvssd  19129  grpinvadd  19130  grpsubf  19131  grpsubrcan  19133  grpinvsub  19134  grpinvval2  19135  grpsubeq0  19138  grpsubadd  19140  grpaddsubass  19142  grpnpcan  19144  dfgrp3  19151  grplactcnv  19155  grpsubpropd2  19158  prdsinvlem  19161  pwssub  19166  imasgrp  19168  ghmgrp  19178  mulgcl  19203  mulgaddcomlem  19209  mulginvcom  19211  mulginvinv  19212  mulgneg2  19220  subginv  19245  subginvcl  19247  issubg4  19258  grpissubg  19259  isnsg3  19272  subgacs  19273  nmzsubg  19277  eqglact  19293  eqgcpbl  19296  qusxpid  19297  qusgrp  19303  qusinv  19307  qussub  19308  eqg0subg  19313  ghminv  19339  ghmsub  19340  ghmrn  19345  ghmpreima  19354  ghmeql  19355  conjghm  19365  galcan  19420  gacan  19421  gapm  19422  gaorber  19424  gastacl  19425  gastacos  19426  cntzsubg  19455  oppggrp  19473  symgsssg  19583  symgfisg  19584  odinv  19677  sylow2blem1  19736  sylow2blem3  19738  frgpuptf  19886  frgpuplem  19888  ablinvadd  19923  ablsub2inv  19924  ablsub4  19926  ablsubsub4  19934  mulgsubdi  19945  invghm  19949  eqgabl  19950  torsubg  19970  oddvdssubg  19971  cyggeninv  19999  ogrpinv0le  20252  ogrpsub  20253  ogrpaddltbi  20255  ogrpaddltrbid  20257  ogrpinv0lt  20259  ogrpinvlt  20260  ringnegl  20433  ringnegr  20434  ringmneg1  20435  ringmneg2  20436  dvdsrneg  20500  unitinvcl  20520  unitnegcl  20527  cntzsubr  20757  isdrng2  20895  isdrng3lem1  20903  abvneg  20981  abvsubtri  20982  orngsqr  21021  lmodvnegcl  21076  lmodvneg1  21078  lmodvsneg  21079  lmodsubvs  21091  lmodsubdi  21092  lmodsubdir  21093  lssvsubcl  21117  lspsnneg  21179  lmodvsinv  21209  lmodvsinv2  21210  lspexch  21305  lspsolvlem  21318  zrhpsgninv  21787  evpmodpmf1o  21798  dsmmsubg  21945  mplsubglem  22200  mplind  22273  cpmatinvcl  22926  chpscmatgsumbin  23053  chpscmatgsummon  23054  tgplacthmeo  24313  tgpconncomp  24323  qustgpopn  24330  tsmsxplem1  24363  tlmtgp  24406  isngp4  24822  ngpinvds  24823  ngpsubcan  24824  nmtri  24836  ngptgp  24846  tngngp3  24866  ncvspi  25368  deg1suble  26317  deg1sub  26318  dchr2sum  27490  dchrisum0re  27730  symgfcoeu  33468  symgsubg  33473  archirngz  33575  archiabllem1b  33578  archiabllem2c  33581  eqgvscpbl  33736  linds2eq  33760  quslsm  33780  nsgmgclem  33786  ressply1sub  33926  madjusmdetlem3  34285  madjusmdetlem4  34286  lflsub  39901  lflnegcl  39909  ldualvsubcl  39990  ldualvsubval  39991  dvhgrp  41941  lcfrlem2  42377  lcdvsubval  42452  mapdpglem30  42536  baerlem3lem1  42541  baerlem5alem1  42542  baerlem5blem1  42543  baerlem5blem2  42546  fldhmf1  42917  nelsubginvcld  43330  invginvrid  49206  lincext1  49293  lindslinindimp2lem1  49297  ldepsprlem  49311  ldepspr  49312  lincresunit3lem3  49313  lincresunit3lem1  49318  lincresunit3lem2  49319  lincresunit3  49320