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

Theorem grpsubval 18793
Description: Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)
Hypotheses
Ref Expression
grpsubval.b 𝐵 = (Base‘𝐺)
grpsubval.p + = (+g𝐺)
grpsubval.i 𝐼 = (invg𝐺)
grpsubval.m = (-g𝐺)
Assertion
Ref Expression
grpsubval ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑋 + (𝐼𝑌)))

Proof of Theorem grpsubval
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7361 . 2 (𝑥 = 𝑋 → (𝑥 + (𝐼𝑦)) = (𝑋 + (𝐼𝑦)))
2 fveq2 6840 . . 3 (𝑦 = 𝑌 → (𝐼𝑦) = (𝐼𝑌))
32oveq2d 7370 . 2 (𝑦 = 𝑌 → (𝑋 + (𝐼𝑦)) = (𝑋 + (𝐼𝑌)))
4 grpsubval.b . . 3 𝐵 = (Base‘𝐺)
5 grpsubval.p . . 3 + = (+g𝐺)
6 grpsubval.i . . 3 𝐼 = (invg𝐺)
7 grpsubval.m . . 3 = (-g𝐺)
84, 5, 6, 7grpsubfval 18791 . 2 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 + (𝐼𝑦)))
9 ovex 7387 . 2 (𝑋 + (𝐼𝑌)) ∈ V
101, 3, 8, 9ovmpo 7512 1 ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑋 + (𝐼𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  cfv 6494  (class class class)co 7354  Basecbs 17080  +gcplusg 17130  invgcminusg 18746  -gcsg 18747
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 2707  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5530  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-fv 6502  df-ov 7357  df-oprab 7358  df-mpo 7359  df-1st 7918  df-2nd 7919  df-sbg 18750
This theorem is referenced by:  grpsubinv  18816  grpsubrcan  18824  grpinvsub  18825  grpinvval2  18826  grpsubid  18827  grpsubid1  18828  grpsubeq0  18829  grpsubadd0sub  18830  grpsubadd  18831  grpsubsub  18832  grpaddsubass  18833  grpnpcan  18835  pwssub  18857  mulgsubdir  18912  subgsubcl  18935  subgsub  18936  issubg4  18943  qussub  18986  ghmsub  19012  sylow2blem1  19398  lsmelvalm  19429  ablsub2inv  19585  ablsub4  19587  ablsubsub4  19593  mulgsubdi  19604  eqgabl  19609  gsumsub  19721  dprdfsub  19796  ringsubdi  20019  ringsubdir  20020  abvsubtri  20290  lmodvsubval2  20373  lmodsubdir  20376  lspsntrim  20555  cnfldsub  20821  m2detleiblem7  21972  chpscmatgsumbin  22189  tgpconncomp  23460  tsmssub  23496  tsmsxplem1  23500  isngp4  23964  ngpsubcan  23966  ngptgp  23988  tngngp3  24016  clmpm1dir  24462  cphipval  24603  deg1suble  25468  deg1sub  25469  dchr2sum  26617  ogrpsub  31819  symgsubg  31833  cycpmconjv  31886  archiabllem2c  31926  linds2eq  32063  ressply1sub  32171  lflsub  37518  ldualvsubval  37608  lcdvsubval  40070  baerlem3lem1  40159  baerlem5alem1  40160  baerlem5amN  40168  baerlem5bmN  40169  baerlem5abmN  40170  hdmapsub  40299  nelsubgsubcld  40661
  Copyright terms: Public domain W3C validator