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

Theorem grpinvcl 15563
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 15562 . 2  |-  ( G  e.  Grp  ->  N : B --> B )
43ffvelrnda 5831 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( N `  X
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362    e. wcel 1755   ` cfv 5406   Basecbs 14157   Grpcgrp 15393   invgcminusg 15394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-0g 14363  df-mnd 15398  df-grp 15525  df-minusg 15526
This theorem is referenced by:  grprinv  15565  grpinvid1  15566  grpinvid2  15567  grplcan  15570  grpinvinv  15573  grpinvcnv  15574  grpinvnzcl  15578  grpsubinv  15579  grplmulf1o  15580  grpinvssd  15583  grpinvadd  15584  grpsubf  15585  grpsubrcan  15587  grpinvsub  15588  grpinvval2  15589  grpsubeq0  15592  grpsubadd  15593  grpaddsubass  15595  grpnpcan  15597  grplactcnv  15604  grpsubpropd2  15607  mulgcl  15624  mulgneg2  15634  prdsinvlem  15643  pwssub  15648  imasgrp  15651  subginv  15668  subginvcl  15670  issubg4  15680  grpissubg  15681  isnsg3  15695  subgacs  15696  nmzsubg  15702  eqger  15711  eqglact  15712  eqgcpbl  15715  divsgrp  15716  divsinv  15720  divssub  15721  ghminv  15734  ghmsub  15735  ghmrn  15740  ghmpreima  15748  ghmeql  15749  conjghm  15757  conjnmz  15760  galcan  15802  gacan  15803  gapm  15804  gaorber  15806  gastacl  15807  gastacos  15808  cntzsubg  15834  oppggrp  15852  symgsssg  15953  symgfisg  15954  odinv  16042  sylow2blem1  16099  sylow2blem3  16101  frgpuptf  16247  frgpuplem  16249  ablinvadd  16279  ablsub2inv  16280  ablsub4  16282  ablsubsub4  16288  mulgsubdi  16297  invghm  16298  eqgabl  16299  torsubg  16316  oddvdssubg  16317  cyggeninv  16340  rngnegl  16620  rngnegr  16621  rngmneg1  16622  rngmneg2  16623  rngm2neg  16624  rngsubdi  16625  rngsubdir  16626  dvdsrneg  16680  unitinvcl  16700  unitnegcl  16707  isdrng2  16766  cntzsubr  16821  abvneg  16843  abvsubtri  16844  lmodvnegcl  16910  lmodvneg1  16912  lmodvsneg  16913  lmodsubvs  16925  lmodsubdi  16926  lmodsubdir  16927  lssvsubcl  16947  lssvnegcl  16959  lspsnneg  17009  lmodvsinv  17039  lmodvsinv2  17040  lspexch  17132  lspsolvlem  17145  mplsubglem  17444  mplsubglemOLD  17446  mplind  17516  zrhpsgninv  17857  evpmodpmf1o  17868  dsmmsubg  18010  tgplacthmeo  19516  tgpconcomp  19525  divstgpopn  19532  tsmsxplem1  19569  tlmtgp  19612  isngp4  20045  ngpinvds  20046  ngpsubcan  20047  nmtri  20059  ngptgp  20064  deg1suble  21464  deg1sub  21465  dchr2sum  22497  dchrisum0re  22647  ogrpinvOLD  26002  ogrpinv0le  26003  ogrpsub  26004  ogrpaddltbi  26006  ogrpaddltrbid  26008  ogrpinv0lt  26010  ogrpinvlt  26011  archirngz  26030  archiabllem1b  26033  archiabllem2c  26036  archiabllem2b  26037  orngsqr  26125  invginvrid  30603  lincext1  30697  lindslinindimp2lem1  30701  ldepsprlem  30715  ldepspr  30716  lincresunit3lem3  30717  lincresunit3lem1  30722  lincresunit3lem2  30723  lincresunit3  30724  lflsub  32285  lflnegcl  32293  ldualvsubcl  32374  ldualvsubval  32375  dvhgrp  34325  lcfrlem2  34761  lcdvsubval  34836  mapdpglem30  34920  baerlem3lem1  34925  baerlem5alem1  34926  baerlem5blem1  34927  baerlem5blem2  34930
  Copyright terms: Public domain W3C validator