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

Theorem grpsubid 18113
Description: Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.)
Hypotheses
Ref Expression
grpsubid.b 𝐵 = (Base‘𝐺)
grpsubid.o 0 = (0g𝐺)
grpsubid.m = (-g𝐺)
Assertion
Ref Expression
grpsubid ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 𝑋) = 0 )

Proof of Theorem grpsubid
StepHypRef Expression
1 grpsubid.b . . . . 5 𝐵 = (Base‘𝐺)
2 eqid 2826 . . . . 5 (+g𝐺) = (+g𝐺)
3 eqid 2826 . . . . 5 (invg𝐺) = (invg𝐺)
4 grpsubid.m . . . . 5 = (-g𝐺)
51, 2, 3, 4grpsubval 18079 . . . 4 ((𝑋𝐵𝑋𝐵) → (𝑋 𝑋) = (𝑋(+g𝐺)((invg𝐺)‘𝑋)))
65anidms 567 . . 3 (𝑋𝐵 → (𝑋 𝑋) = (𝑋(+g𝐺)((invg𝐺)‘𝑋)))
76adantl 482 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 𝑋) = (𝑋(+g𝐺)((invg𝐺)‘𝑋)))
8 grpsubid.o . . 3 0 = (0g𝐺)
91, 2, 8, 3grprinv 18083 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋(+g𝐺)((invg𝐺)‘𝑋)) = 0 )
107, 9eqtrd 2861 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 𝑋) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  cfv 6352  (class class class)co 7148  Basecbs 16473  +gcplusg 16555  0gc0g 16703  Grpcgrp 18033  invgcminusg 18034  -gcsg 18035
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-fv 6360  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-1st 7680  df-2nd 7681  df-0g 16705  df-mgm 17842  df-sgrp 17890  df-mnd 17901  df-grp 18036  df-minusg 18037  df-sbg 18038
This theorem is referenced by:  grppncan  18120  grpnpncan0  18125  issubg4  18228  0nsg  18251  gexdvds  18629  abladdsub4  18854  ablpncan2  18856  ablpnpcan  18860  ablnncan  18861  telgsums  19033  dprdfeq0  19064  lmodsubid  19614  dmatsubcl  21023  mdetuni0  21146  chpmat0d  21358  chpdmatlem2  21363  tgpconncomp  22636  tgpt0  22642  tgptsmscls  22673  deg1sublt  24619  lgsqrlem1  25836  archiabllem1a  30734  archiabllem2a  30737  archiabllem2c  30738  ornglmulle  30792  orngrmulle  30793  lfl0  36068  eqlkr  36102  lkrlsp  36105  lclkrlem2m  38522  lcfrlem1  38545  hdmapinvlem3  38923
  Copyright terms: Public domain W3C validator