MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpinvcl Structured version   Visualization version   GIF version

Theorem grpinvcl 17399
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
StepHypRef Expression
1 grpinvcl.b . . 3 𝐵 = (Base‘𝐺)
2 grpinvcl.n . . 3 𝑁 = (invg𝐺)
31, 2grpinvf 17398 . 2 (𝐺 ∈ Grp → 𝑁:𝐵𝐵)
43ffvelrnda 6320 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  cfv 5852  Basecbs 15792  Grpcgrp 17354  invgcminusg 17355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-0g 16034  df-mgm 17174  df-sgrp 17216  df-mnd 17227  df-grp 17357  df-minusg 17358
This theorem is referenced by:  grprinv  17401  grpinvid1  17402  grpinvid2  17403  grplrinv  17405  grplcan  17409  grpasscan1  17410  grpasscan2  17411  grpinvinv  17414  grpinvcnv  17415  grpinvnzcl  17419  grpsubinv  17420  grplmulf1o  17421  grpinvssd  17424  grpinvadd  17425  grpsubf  17426  grpsubrcan  17428  grpinvsub  17429  grpinvval2  17430  grpsubeq0  17433  grpsubadd  17435  grpaddsubass  17437  grpnpcan  17439  dfgrp3  17446  grplactcnv  17450  grpsubpropd2  17453  prdsinvlem  17456  pwssub  17461  imasgrp  17463  ghmgrp  17471  mulgcl  17491  mulgaddcomlem  17495  mulginvcom  17497  mulginvinv  17498  mulgneg2  17507  subginv  17533  subginvcl  17535  issubg4  17545  grpissubg  17546  isnsg3  17560  subgacs  17561  nmzsubg  17567  eqger  17576  eqglact  17577  eqgcpbl  17580  qusgrp  17581  qusinv  17585  qussub  17586  ghminv  17599  ghmsub  17600  ghmrn  17605  ghmpreima  17614  ghmeql  17615  conjghm  17623  conjnmz  17626  galcan  17669  gacan  17670  gapm  17671  gaorber  17673  gastacl  17674  gastacos  17675  cntzsubg  17701  oppggrp  17719  symgsssg  17819  symgfisg  17820  odinv  17910  sylow2blem1  17967  sylow2blem3  17969  frgpuptf  18115  frgpuplem  18117  ablinvadd  18147  ablsub2inv  18148  ablsub4  18150  ablsubsub4  18156  mulgsubdi  18167  invghm  18171  eqgabl  18172  torsubg  18189  oddvdssubg  18190  cyggeninv  18217  ringnegl  18526  rngnegr  18527  ringmneg1  18528  ringmneg2  18529  ringm2neg  18530  ringsubdi  18531  rngsubdir  18532  dvdsrneg  18586  unitinvcl  18606  unitnegcl  18613  isdrng2  18689  cntzsubr  18744  abvneg  18766  abvsubtri  18767  lmodvnegcl  18836  lmodvneg1  18838  lmodvsneg  18839  lmodsubvs  18851  lmodsubdi  18852  lmodsubdir  18853  lssvsubcl  18876  lssvnegcl  18888  lspsnneg  18938  lmodvsinv  18968  lmodvsinv2  18969  lspexch  19061  lspsolvlem  19074  mplsubglem  19366  mplind  19434  zrhpsgninv  19863  evpmodpmf1o  19874  dsmmsubg  20019  cpmatinvcl  20454  chpscmatgsumbin  20581  chpscmatgsummon  20582  tgplacthmeo  21830  tgpconncomp  21839  qustgpopn  21846  tsmsxplem1  21879  tlmtgp  21922  isngp4  22339  ngpinvds  22340  ngpsubcan  22341  nmtri  22353  ngptgp  22363  tngngp3  22383  ncvspi  22879  deg1suble  23788  deg1sub  23789  dchr2sum  24915  dchrisum0re  25119  ogrpinvOLD  29524  ogrpinv0le  29525  ogrpsub  29526  ogrpaddltbi  29528  ogrpaddltrbid  29530  ogrpinv0lt  29532  ogrpinvlt  29533  archirngz  29552  archiabllem1b  29555  archiabllem2c  29558  orngsqr  29613  symgfcoeu  29654  madjusmdetlem3  29701  madjusmdetlem4  29702  lflsub  33869  lflnegcl  33877  ldualvsubcl  33958  ldualvsubval  33959  dvhgrp  35911  lcfrlem2  36347  lcdvsubval  36422  mapdpglem30  36506  baerlem3lem1  36511  baerlem5alem1  36512  baerlem5blem1  36513  baerlem5blem2  36516  invginvrid  41462  lincext1  41557  lindslinindimp2lem1  41561  ldepsprlem  41575  ldepspr  41576  lincresunit3lem3  41577  lincresunit3lem1  41582  lincresunit3lem2  41583  lincresunit3  41584
  Copyright terms: Public domain W3C validator