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

Theorem grpinvcl 16221
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 16220 . 2  |-  ( G  e.  Grp  ->  N : B --> B )
43ffvelrnda 6032 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( N `  X
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395    e. wcel 1819   ` cfv 5594   Basecbs 14643   Grpcgrp 16179   invgcminusg 16180
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-0g 14858  df-mgm 15998  df-sgrp 16037  df-mnd 16047  df-grp 16183  df-minusg 16184
This theorem is referenced by:  grprinv  16223  grpinvid1  16224  grpinvid2  16225  grplcan  16228  grpinvinv  16231  grpinvcnv  16232  grpinvnzcl  16236  grpsubinv  16237  grplmulf1o  16238  grpinvssd  16241  grpinvadd  16242  grpsubf  16243  grpsubrcan  16245  grpinvsub  16246  grpinvval2  16247  grpsubeq0  16250  grpsubadd  16252  grpaddsubass  16254  grpnpcan  16256  grplactcnv  16264  grpsubpropd2  16267  mulgcl  16285  mulgneg2  16295  prdsinvlem  16304  pwssub  16309  imasgrp  16312  ghmgrp  16320  subginv  16334  subginvcl  16336  issubg4  16346  grpissubg  16347  isnsg3  16361  subgacs  16362  nmzsubg  16368  eqger  16377  eqglact  16378  eqgcpbl  16381  qusgrp  16382  qusinv  16386  qussub  16387  ghminv  16400  ghmsub  16401  ghmrn  16406  ghmpreima  16414  ghmeql  16415  conjghm  16423  conjnmz  16426  galcan  16468  gacan  16469  gapm  16470  gaorber  16472  gastacl  16473  gastacos  16474  cntzsubg  16500  oppggrp  16518  symgsssg  16618  symgfisg  16619  odinv  16709  sylow2blem1  16766  sylow2blem3  16768  frgpuptf  16914  frgpuplem  16916  ablinvadd  16946  ablsub2inv  16947  ablsub4  16949  ablsubsub4  16955  mulgsubdi  16964  invghm  16968  eqgabl  16969  torsubg  16986  oddvdssubg  16987  cyggeninv  17012  ringnegl  17366  rngnegr  17367  ringmneg1  17368  ringmneg2  17369  ringm2neg  17370  ringsubdi  17371  rngsubdir  17372  dvdsrneg  17429  unitinvcl  17449  unitnegcl  17456  isdrng2  17532  cntzsubr  17587  abvneg  17609  abvsubtri  17610  lmodvnegcl  17677  lmodvneg1  17679  lmodvsneg  17680  lmodsubvs  17692  lmodsubdi  17693  lmodsubdir  17694  lssvsubcl  17716  lssvnegcl  17728  lspsnneg  17778  lmodvsinv  17808  lmodvsinv2  17809  lspexch  17901  lspsolvlem  17914  mplsubglem  18219  mplsubglemOLD  18221  mplind  18293  zrhpsgninv  18747  evpmodpmf1o  18758  dsmmsubg  18900  cpmatinvcl  19344  chpscmatgsumbin  19471  chpscmatgsummon  19472  tgplacthmeo  20727  tgpconcomp  20736  qustgpopn  20743  tsmsxplem1  20780  tlmtgp  20823  isngp4  21256  ngpinvds  21257  ngpsubcan  21258  nmtri  21270  ngptgp  21275  deg1suble  22633  deg1sub  22634  dchr2sum  23673  dchrisum0re  23823  ogrpinvOLD  27857  ogrpinv0le  27858  ogrpsub  27859  ogrpaddltbi  27861  ogrpaddltrbid  27863  ogrpinv0lt  27865  ogrpinvlt  27866  archirngz  27885  archiabllem1b  27888  archiabllem2c  27891  orngsqr  27947  invginvrid  33062  lincext1  33157  lindslinindimp2lem1  33161  ldepsprlem  33175  ldepspr  33176  lincresunit3lem3  33177  lincresunit3lem1  33182  lincresunit3lem2  33183  lincresunit3  33184  lflsub  34893  lflnegcl  34901  ldualvsubcl  34982  ldualvsubval  34983  dvhgrp  36935  lcfrlem2  37371  lcdvsubval  37446  mapdpglem30  37530  baerlem3lem1  37535  baerlem5alem1  37536  baerlem5blem1  37537  baerlem5blem2  37540
  Copyright terms: Public domain W3C validator