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

Theorem grprinv 18131
Description: The right inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
grpinv.b 𝐵 = (Base‘𝐺)
grpinv.p + = (+g𝐺)
grpinv.u 0 = (0g𝐺)
grpinv.n 𝑁 = (invg𝐺)
Assertion
Ref Expression
grprinv ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 + (𝑁𝑋)) = 0 )

Proof of Theorem grprinv
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grpinv.b . . 3 𝐵 = (Base‘𝐺)
2 grpinv.p . . 3 + = (+g𝐺)
31, 2grpcl 18089 . 2 ((𝐺 ∈ Grp ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
4 grpinv.u . . 3 0 = (0g𝐺)
51, 4grpidcl 18109 . 2 (𝐺 ∈ Grp → 0𝐵)
61, 2, 4grplid 18111 . 2 ((𝐺 ∈ Grp ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
71, 2grpass 18090 . 2 ((𝐺 ∈ Grp ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
81, 2, 4grpinvex 18091 . 2 ((𝐺 ∈ Grp ∧ 𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 0 )
9 simpr 488 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → 𝑋𝐵)
10 grpinv.n . . 3 𝑁 = (invg𝐺)
111, 10grpinvcl 18129 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)
121, 2, 4, 10grplinv 18130 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → ((𝑁𝑋) + 𝑋) = 0 )
133, 5, 6, 7, 8, 9, 11, 12grprinvd 17862 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 + (𝑁𝑋)) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2115  cfv 6328  (class class class)co 7130  Basecbs 16461  +gcplusg 16543  0gc0g 16691  Grpcgrp 18081  invgcminusg 18082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336  df-riota 7088  df-ov 7133  df-0g 16693  df-mgm 17830  df-sgrp 17879  df-mnd 17890  df-grp 18084  df-minusg 18085
This theorem is referenced by:  grpinvid1  18132  grpinvid2  18133  grplrinv  18135  grpasscan1  18140  grpinvinv  18144  grplmulf1o  18151  grpinvadd  18155  grpsubid  18161  dfgrp3  18176  mulgdirlem  18236  subginv  18264  nmzsubg  18295  eqger  18308  qusinv  18317  ghminv  18343  conjnmz  18370  gacan  18413  cntzsubg  18445  oppggrp  18463  oppginv  18465  psgnuni  18605  sylow2blem3  18725  frgpuplem  18876  ringnegl  19322  unitrinv  19406  isdrng2  19487  lmodvnegid  19651  lmodvsinv2  19784  lspsolvlem  19889  evpmodpmf1o  20715  grpvrinv  20982  mdetralt  21192  ghmcnp  22698  qustgpopn  22703  isngp4  23196  clmvsrinv  23690  ogrpinv0le  30723  ogrpaddltbi  30726  ogrpinv0lt  30730  ogrpinvlt  30731  archiabllem1b  30828  orngsqr  30884  lbsdiflsp0  31032  ldepsprlem  44672
  Copyright terms: Public domain W3C validator