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

Theorem hvsubval 27039
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 6438 . 2 (𝑥 = 𝐴 → (𝑥 + (-1 · 𝑦)) = (𝐴 + (-1 · 𝑦)))
2 oveq2 6439 . . 3 (𝑦 = 𝐵 → (-1 · 𝑦) = (-1 · 𝐵))
32oveq2d 6447 . 2 (𝑦 = 𝐵 → (𝐴 + (-1 · 𝑦)) = (𝐴 + (-1 · 𝐵)))
4 df-hvsub 26994 . 2 = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 + (-1 · 𝑦)))
5 ovex 6459 . 2 (𝐴 + (-1 · 𝐵)) ∈ V
61, 3, 4, 5ovmpt2 6576 1 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 𝐵) = (𝐴 + (-1 · 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1938  (class class class)co 6431  1c1 9696  -cneg 10021  chil 26942   + cva 26943   · csm 26944   cmv 26948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-iota 5658  df-fun 5696  df-fv 5702  df-ov 6434  df-oprab 6435  df-mpt2 6436  df-hvsub 26994
This theorem is referenced by:  hvsubcl  27040  hvsubvali  27043  hvsubid  27049  hvnegid  27050  hv2neg  27051  hvaddsubval  27056  hvsub4  27060  hvaddsub12  27061  hvpncan  27062  hvaddsubass  27064  hvsubass  27067  hvsubdistr1  27072  hvsubdistr2  27073  hvsubcan  27097  hvsub0  27099  his2sub  27115  hhph  27201  shsubcl  27243  shsel3  27340  honegsubi  27821  lnopsubi  27999  lnfnsubi  28071  superpos  28379  cdj1i  28458
  Copyright terms: Public domain W3C validator