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

Theorem grpinvcl 17589
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 17588 . 2 (𝐺 ∈ Grp → 𝑁:𝐵𝐵)
43ffvelrnda 6474 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1596  wcel 2103  cfv 6001  Basecbs 15980  Grpcgrp 17544  invgcminusg 17545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-0g 16225  df-mgm 17364  df-sgrp 17406  df-mnd 17417  df-grp 17547  df-minusg 17548
This theorem is referenced by:  grprinv  17591  grpinvid1  17592  grpinvid2  17593  grplrinv  17595  grplcan  17599  grpasscan1  17600  grpasscan2  17601  grpinvinv  17604  grpinvcnv  17605  grpinvnzcl  17609  grpsubinv  17610  grplmulf1o  17611  grpinvssd  17614  grpinvadd  17615  grpsubf  17616  grpsubrcan  17618  grpinvsub  17619  grpinvval2  17620  grpsubeq0  17623  grpsubadd  17625  grpaddsubass  17627  grpnpcan  17629  dfgrp3  17636  grplactcnv  17640  grpsubpropd2  17643  prdsinvlem  17646  pwssub  17651  imasgrp  17653  ghmgrp  17661  mulgcl  17681  mulgaddcomlem  17685  mulginvcom  17687  mulginvinv  17688  mulgneg2  17697  subginv  17723  subginvcl  17725  issubg4  17735  grpissubg  17736  isnsg3  17750  subgacs  17751  nmzsubg  17757  eqger  17766  eqglact  17767  eqgcpbl  17770  qusgrp  17771  qusinv  17775  qussub  17776  ghminv  17789  ghmsub  17790  ghmrn  17795  ghmpreima  17804  ghmeql  17805  conjghm  17813  conjnmz  17816  galcan  17858  gacan  17859  gapm  17860  gaorber  17862  gastacl  17863  gastacos  17864  cntzsubg  17890  oppggrp  17908  symgsssg  18008  symgfisg  18009  odinv  18099  sylow2blem1  18156  sylow2blem3  18158  frgpuptf  18304  frgpuplem  18306  ablinvadd  18336  ablsub2inv  18337  ablsub4  18339  ablsubsub4  18345  mulgsubdi  18356  invghm  18360  eqgabl  18361  torsubg  18378  oddvdssubg  18379  cyggeninv  18406  ringnegl  18715  rngnegr  18716  ringmneg1  18717  ringmneg2  18718  ringm2neg  18719  ringsubdi  18720  rngsubdir  18721  dvdsrneg  18775  unitinvcl  18795  unitnegcl  18802  isdrng2  18880  cntzsubr  18935  abvneg  18957  abvsubtri  18958  lmodvnegcl  19027  lmodvneg1  19029  lmodvsneg  19030  lmodsubvs  19042  lmodsubdi  19043  lmodsubdir  19044  lssvsubcl  19067  lssvnegcl  19079  lspsnneg  19129  lmodvsinv  19159  lmodvsinv2  19160  lspexch  19252  lspsolvlem  19265  mplsubglem  19557  mplind  19625  zrhpsgninv  20054  evpmodpmf1o  20065  dsmmsubg  20210  cpmatinvcl  20645  chpscmatgsumbin  20772  chpscmatgsummon  20773  tgplacthmeo  22029  tgpconncomp  22038  qustgpopn  22045  tsmsxplem1  22078  tlmtgp  22121  isngp4  22538  ngpinvds  22539  ngpsubcan  22540  nmtri  22552  ngptgp  22562  tngngp3  22582  ncvspi  23077  deg1suble  23987  deg1sub  23988  dchr2sum  25118  dchrisum0re  25322  ogrpinvOLD  29945  ogrpinv0le  29946  ogrpsub  29947  ogrpaddltbi  29949  ogrpaddltrbid  29951  ogrpinv0lt  29953  ogrpinvlt  29954  archirngz  29973  archiabllem1b  29976  archiabllem2c  29979  orngsqr  30034  symgfcoeu  30075  madjusmdetlem3  30125  madjusmdetlem4  30126  lflsub  34774  lflnegcl  34782  ldualvsubcl  34863  ldualvsubval  34864  dvhgrp  36815  lcfrlem2  37251  lcdvsubval  37326  mapdpglem30  37410  baerlem3lem1  37415  baerlem5alem1  37416  baerlem5blem1  37417  baerlem5blem2  37420  invginvrid  42575  lincext1  42670  lindslinindimp2lem1  42674  ldepsprlem  42688  ldepspr  42689  lincresunit3lem3  42690  lincresunit3lem1  42695  lincresunit3lem2  42696  lincresunit3  42697
  Copyright terms: Public domain W3C validator