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

Theorem grprinv 18917
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 18868 . 2 ((𝐺 ∈ Grp ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
4 grpinv.u . . 3 0 = (0g𝐺)
51, 4grpidcl 18892 . 2 (𝐺 ∈ Grp → 0𝐵)
61, 2, 4grplid 18894 . 2 ((𝐺 ∈ Grp ∧ 𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
71, 2grpass 18869 . 2 ((𝐺 ∈ Grp ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
81, 2, 4grpinvex 18870 . 2 ((𝐺 ∈ Grp ∧ 𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 0 )
9 simpr 484 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → 𝑋𝐵)
10 grpinv.n . . 3 𝑁 = (invg𝐺)
111, 10grpinvcl 18914 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)
121, 2, 4, 10grplinv 18916 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → ((𝑁𝑋) + 𝑋) = 0 )
133, 5, 6, 7, 8, 9, 11, 12grpinva 18604 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 + (𝑁𝑋)) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1533  wcel 2098  cfv 6536  (class class class)co 7404  Basecbs 17150  +gcplusg 17203  0gc0g 17391  Grpcgrp 18860  invgcminusg 18861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-riota 7360  df-ov 7407  df-0g 17393  df-mgm 18570  df-sgrp 18649  df-mnd 18665  df-grp 18863  df-minusg 18864
This theorem is referenced by:  grpinvid1  18918  grpinvid2  18919  grprinvd  18922  grplrinv  18923  grpasscan1  18928  grpinvinv  18932  grplmulf1o  18939  grpinvadd  18943  grpsubid  18949  dfgrp3  18964  mulgdirlem  19029  subginv  19057  nmzsubg  19089  eqger  19102  qusinv  19113  ghminv  19145  conjnmz  19174  gacan  19218  cntzsubg  19252  oppggrp  19273  oppginv  19275  psgnuni  19416  sylow2blem3  19539  frgpuplem  19689  ringnegl  20198  unitrinv  20293  isdrng2  20598  lmodvnegid  20747  lmodvsinv2  20882  lspsolvlem  20990  evpmodpmf1o  21484  grpvrinv  22248  mdetralt  22460  ghmcnp  23969  qustgpopn  23974  isngp4  24471  clmvsrinv  24984  ogrpinv0le  32736  ogrpaddltbi  32739  ogrpinv0lt  32743  ogrpinvlt  32744  archiabllem1b  32841  orngsqr  32924  quslsm  33021  lbsdiflsp0  33228  fldhmf1  41470  ldepsprlem  47410
  Copyright terms: Public domain W3C validator