HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  hvsubval Structured version   Visualization version   GIF version

Theorem hvsubval 28449
Description: Value of vector subtraction. (Contributed by NM, 5-Sep-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
hvsubval ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 𝐵) = (𝐴 + (-1 · 𝐵)))

Proof of Theorem hvsubval
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6931 . 2 (𝑥 = 𝐴 → (𝑥 + (-1 · 𝑦)) = (𝐴 + (-1 · 𝑦)))
2 oveq2 6932 . . 3 (𝑦 = 𝐵 → (-1 · 𝑦) = (-1 · 𝐵))
32oveq2d 6940 . 2 (𝑦 = 𝐵 → (𝐴 + (-1 · 𝑦)) = (𝐴 + (-1 · 𝐵)))
4 df-hvsub 28404 . 2 = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 + (-1 · 𝑦)))
5 ovex 6956 . 2 (𝐴 + (-1 · 𝐵)) ∈ V
61, 3, 4, 5ovmpt2 7075 1 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 𝐵) = (𝐴 + (-1 · 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2107  (class class class)co 6924  1c1 10275  -cneg 10609  chba 28352   + cva 28353   · csm 28354   cmv 28358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-iota 6101  df-fun 6139  df-fv 6145  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-hvsub 28404
This theorem is referenced by:  hvsubcl  28450  hvsubvali  28453  hvsubid  28459  hvnegid  28460  hv2neg  28461  hvaddsubval  28466  hvsub4  28470  hvaddsub12  28471  hvpncan  28472  hvaddsubass  28474  hvsubass  28477  hvsubdistr1  28482  hvsubdistr2  28483  hvsubcan  28507  hvsub0  28509  his2sub  28525  hhph  28611  shsubcl  28653  shsel3  28750  honegsubi  29231  lnopsubi  29409  lnfnsubi  29481  superpos  29789  cdj1i  29868
  Copyright terms: Public domain W3C validator