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

Theorem grpinvcl 15574
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 15573 . 2  |-  ( G  e.  Grp  ->  N : B --> B )
43ffvelrnda 5838 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( N `  X
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   ` cfv 5413   Basecbs 14166   Grpcgrp 15402   invgcminusg 15403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-0g 14372  df-mnd 15407  df-grp 15536  df-minusg 15537
This theorem is referenced by:  grprinv  15576  grpinvid1  15577  grpinvid2  15578  grplcan  15581  grpinvinv  15584  grpinvcnv  15585  grpinvnzcl  15589  grpsubinv  15590  grplmulf1o  15591  grpinvssd  15594  grpinvadd  15595  grpsubf  15596  grpsubrcan  15598  grpinvsub  15599  grpinvval2  15600  grpsubeq0  15603  grpsubadd  15604  grpaddsubass  15606  grpnpcan  15608  grplactcnv  15615  grpsubpropd2  15618  mulgcl  15635  mulgneg2  15645  prdsinvlem  15654  pwssub  15659  imasgrp  15662  subginv  15679  subginvcl  15681  issubg4  15691  grpissubg  15692  isnsg3  15706  subgacs  15707  nmzsubg  15713  eqger  15722  eqglact  15723  eqgcpbl  15726  divsgrp  15727  divsinv  15731  divssub  15732  ghminv  15745  ghmsub  15746  ghmrn  15751  ghmpreima  15759  ghmeql  15760  conjghm  15768  conjnmz  15771  galcan  15813  gacan  15814  gapm  15815  gaorber  15817  gastacl  15818  gastacos  15819  cntzsubg  15845  oppggrp  15863  symgsssg  15964  symgfisg  15965  odinv  16053  sylow2blem1  16110  sylow2blem3  16112  frgpuptf  16258  frgpuplem  16260  ablinvadd  16290  ablsub2inv  16291  ablsub4  16293  ablsubsub4  16299  mulgsubdi  16308  invghm  16309  eqgabl  16310  torsubg  16327  oddvdssubg  16328  cyggeninv  16351  rngnegl  16673  rngnegr  16674  rngmneg1  16675  rngmneg2  16676  rngm2neg  16677  rngsubdi  16678  rngsubdir  16679  dvdsrneg  16734  unitinvcl  16754  unitnegcl  16761  isdrng2  16820  cntzsubr  16875  abvneg  16897  abvsubtri  16898  lmodvnegcl  16964  lmodvneg1  16966  lmodvsneg  16967  lmodsubvs  16979  lmodsubdi  16980  lmodsubdir  16981  lssvsubcl  17002  lssvnegcl  17014  lspsnneg  17064  lmodvsinv  17094  lmodvsinv2  17095  lspexch  17187  lspsolvlem  17200  mplsubglem  17487  mplsubglemOLD  17489  mplind  17559  zrhpsgninv  17990  evpmodpmf1o  18001  dsmmsubg  18143  tgplacthmeo  19649  tgpconcomp  19658  divstgpopn  19665  tsmsxplem1  19702  tlmtgp  19745  isngp4  20178  ngpinvds  20179  ngpsubcan  20180  nmtri  20192  ngptgp  20197  deg1suble  21554  deg1sub  21555  dchr2sum  22587  dchrisum0re  22737  ogrpinvOLD  26129  ogrpinv0le  26130  ogrpsub  26131  ogrpaddltbi  26133  ogrpaddltrbid  26135  ogrpinv0lt  26137  ogrpinvlt  26138  archirngz  26157  archiabllem1b  26160  archiabllem2c  26163  archiabllem2b  26164  orngsqr  26223  invginvrid  30723  lincext1  30877  lindslinindimp2lem1  30881  ldepsprlem  30895  ldepspr  30896  lincresunit3lem3  30897  lincresunit3lem1  30902  lincresunit3lem2  30903  lincresunit3  30904  lflsub  32552  lflnegcl  32560  ldualvsubcl  32641  ldualvsubval  32642  dvhgrp  34592  lcfrlem2  35028  lcdvsubval  35103  mapdpglem30  35187  baerlem3lem1  35192  baerlem5alem1  35193  baerlem5blem1  35194  baerlem5blem2  35197
  Copyright terms: Public domain W3C validator