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

Theorem grpnpcan 18891
Description: Cancellation law for subtraction (npcan 11453 analog). (Contributed by NM, 19-Apr-2014.)
Hypotheses
Ref Expression
grpsubadd.b 𝐵 = (Base‘𝐺)
grpsubadd.p + = (+g𝐺)
grpsubadd.m = (-g𝐺)
Assertion
Ref Expression
grpnpcan ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌) + 𝑌) = 𝑋)

Proof of Theorem grpnpcan
StepHypRef Expression
1 grpsubadd.b . . . . . 6 𝐵 = (Base‘𝐺)
2 eqid 2732 . . . . . 6 (invg𝐺) = (invg𝐺)
31, 2grpinvcl 18849 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌𝐵) → ((invg𝐺)‘𝑌) ∈ 𝐵)
433adant2 1131 . . . 4 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((invg𝐺)‘𝑌) ∈ 𝐵)
5 grpsubadd.p . . . . 5 + = (+g𝐺)
61, 5grpcl 18804 . . . 4 ((𝐺 ∈ Grp ∧ 𝑋𝐵 ∧ ((invg𝐺)‘𝑌) ∈ 𝐵) → (𝑋 + ((invg𝐺)‘𝑌)) ∈ 𝐵)
74, 6syld3an3 1409 . . 3 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + ((invg𝐺)‘𝑌)) ∈ 𝐵)
8 grpsubadd.m . . . 4 = (-g𝐺)
91, 5, 2, 8grpsubval 18847 . . 3 (((𝑋 + ((invg𝐺)‘𝑌)) ∈ 𝐵 ∧ ((invg𝐺)‘𝑌) ∈ 𝐵) → ((𝑋 + ((invg𝐺)‘𝑌)) ((invg𝐺)‘𝑌)) = ((𝑋 + ((invg𝐺)‘𝑌)) + ((invg𝐺)‘((invg𝐺)‘𝑌))))
107, 4, 9syl2anc 584 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 + ((invg𝐺)‘𝑌)) ((invg𝐺)‘𝑌)) = ((𝑋 + ((invg𝐺)‘𝑌)) + ((invg𝐺)‘((invg𝐺)‘𝑌))))
111, 5, 8grppncan 18890 . . 3 ((𝐺 ∈ Grp ∧ 𝑋𝐵 ∧ ((invg𝐺)‘𝑌) ∈ 𝐵) → ((𝑋 + ((invg𝐺)‘𝑌)) ((invg𝐺)‘𝑌)) = 𝑋)
124, 11syld3an3 1409 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 + ((invg𝐺)‘𝑌)) ((invg𝐺)‘𝑌)) = 𝑋)
131, 5, 2, 8grpsubval 18847 . . . . 5 ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑋 + ((invg𝐺)‘𝑌)))
14133adant1 1130 . . . 4 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑋 + ((invg𝐺)‘𝑌)))
1514eqcomd 2738 . . 3 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + ((invg𝐺)‘𝑌)) = (𝑋 𝑌))
161, 2grpinvinv 18866 . . . 4 ((𝐺 ∈ Grp ∧ 𝑌𝐵) → ((invg𝐺)‘((invg𝐺)‘𝑌)) = 𝑌)
17163adant2 1131 . . 3 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((invg𝐺)‘((invg𝐺)‘𝑌)) = 𝑌)
1815, 17oveq12d 7412 . 2 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 + ((invg𝐺)‘𝑌)) + ((invg𝐺)‘((invg𝐺)‘𝑌))) = ((𝑋 𝑌) + 𝑌))
1910, 12, 183eqtr3rd 2781 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌) + 𝑌) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087   = wceq 1541  wcel 2106  cfv 6533  (class class class)co 7394  Basecbs 17128  +gcplusg 17181  Grpcgrp 18796  invgcminusg 18797  -gcsg 18798
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-1st 7959  df-2nd 7960  df-0g 17371  df-mgm 18545  df-sgrp 18594  df-mnd 18605  df-grp 18799  df-minusg 18800  df-sbg 18801
This theorem is referenced by:  grpsubsub4  18892  grpnpncan  18894  grpnnncan2  18896  dfgrp3  18898  nsgconj  19013  conjghm  19091  conjnmz  19094  sylow2blem1  19454  ablpncan3  19647  lmodvnpcan  20477  ipsubdir  21130  ipsubdi  21131  coe1subfv  21721  mdetunilem9  22053  subgntr  23542  ghmcnp  23550  tgpt0  23554  r1pid  25608  archiabllem1a  32272  archiabllem2a  32275  ornglmulle  32349  orngrmulle  32350  kercvrlsm  41660  hbtlem5  41705
  Copyright terms: Public domain W3C validator