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

Theorem grpinvcl 16698
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  |-  B  =  ( Base `  G
)
grpinvcl.n  |-  N  =  ( invg `  G )
Assertion
Ref Expression
grpinvcl  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( N `  X
)  e.  B )

Proof of Theorem grpinvcl
StepHypRef Expression
1 grpinvcl.b . . 3  |-  B  =  ( Base `  G
)
2 grpinvcl.n . . 3  |-  N  =  ( invg `  G )
31, 2grpinvf 16697 . 2  |-  ( G  e.  Grp  ->  N : B --> B )
43ffvelrnda 6033 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( N `  X
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1868   ` cfv 5597   Basecbs 15108   Grpcgrp 16656   invgcminusg 16657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-0g 15327  df-mgm 16475  df-sgrp 16514  df-mnd 16524  df-grp 16660  df-minusg 16661
This theorem is referenced by:  grprinv  16700  grpinvid1  16701  grpinvid2  16702  grplcan  16705  grpinvinv  16708  grpinvcnv  16709  grpinvnzcl  16713  grpsubinv  16714  grplmulf1o  16715  grpinvssd  16718  grpinvadd  16719  grpsubf  16720  grpsubrcan  16722  grpinvsub  16723  grpinvval2  16724  grpsubeq0  16727  grpsubadd  16729  grpaddsubass  16731  grpnpcan  16733  grplactcnv  16741  grpsubpropd2  16744  mulgcl  16762  mulgneg2  16772  prdsinvlem  16781  pwssub  16786  imasgrp  16789  ghmgrp  16797  subginv  16811  subginvcl  16813  issubg4  16823  grpissubg  16824  isnsg3  16838  subgacs  16839  nmzsubg  16845  eqger  16854  eqglact  16855  eqgcpbl  16858  qusgrp  16859  qusinv  16863  qussub  16864  ghminv  16877  ghmsub  16878  ghmrn  16883  ghmpreima  16891  ghmeql  16892  conjghm  16900  conjnmz  16903  galcan  16945  gacan  16946  gapm  16947  gaorber  16949  gastacl  16950  gastacos  16951  cntzsubg  16977  oppggrp  16995  symgsssg  17095  symgfisg  17096  odinv  17199  sylow2blem1  17259  sylow2blem3  17261  frgpuptf  17407  frgpuplem  17409  ablinvadd  17439  ablsub2inv  17440  ablsub4  17442  ablsubsub4  17448  mulgsubdi  17457  invghm  17461  eqgabl  17462  torsubg  17479  oddvdssubg  17480  cyggeninv  17505  ringnegl  17809  rngnegr  17810  ringmneg1  17811  ringmneg2  17812  ringm2neg  17813  ringsubdi  17814  rngsubdir  17815  dvdsrneg  17869  unitinvcl  17889  unitnegcl  17896  isdrng2  17972  cntzsubr  18027  abvneg  18049  abvsubtri  18050  lmodvnegcl  18116  lmodvneg1  18118  lmodvsneg  18119  lmodsubvs  18131  lmodsubdi  18132  lmodsubdir  18133  lssvsubcl  18154  lssvnegcl  18166  lspsnneg  18216  lmodvsinv  18246  lmodvsinv2  18247  lspexch  18339  lspsolvlem  18352  mplsubglem  18645  mplind  18712  zrhpsgninv  19139  evpmodpmf1o  19150  dsmmsubg  19292  cpmatinvcl  19727  chpscmatgsumbin  19854  chpscmatgsummon  19855  tgplacthmeo  21104  tgpconcomp  21113  qustgpopn  21120  tsmsxplem1  21153  tlmtgp  21196  isngp4  21611  ngpinvds  21612  ngpsubcan  21613  nmtri  21625  ngptgp  21630  deg1suble  23042  deg1sub  23043  dchr2sum  24187  dchrisum0re  24337  ogrpinvOLD  28472  ogrpinv0le  28473  ogrpsub  28474  ogrpaddltbi  28476  ogrpaddltrbid  28478  ogrpinv0lt  28480  ogrpinvlt  28481  archirngz  28500  archiabllem1b  28503  archiabllem2c  28506  orngsqr  28562  symgfcoeu  28603  madjusmdetlem3  28650  madjusmdetlem4  28651  lflsub  32551  lflnegcl  32559  ldualvsubcl  32640  ldualvsubval  32641  dvhgrp  34593  lcfrlem2  35029  lcdvsubval  35104  mapdpglem30  35188  baerlem3lem1  35193  baerlem5alem1  35194  baerlem5blem1  35195  baerlem5blem2  35198  invginvrid  39425  lincext1  39520  lindslinindimp2lem1  39524  ldepsprlem  39538  ldepspr  39539  lincresunit3lem3  39540  lincresunit3lem1  39545  lincresunit3lem2  39546  lincresunit3  39547
  Copyright terms: Public domain W3C validator