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

Theorem hvaddlidi 31048
Description: Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
Hypothesis
Ref Expression
hvaddlid.1 𝐴 ∈ ℋ
Assertion
Ref Expression
hvaddlidi (0 + 𝐴) = 𝐴

Proof of Theorem hvaddlidi
StepHypRef Expression
1 hvaddlid.1 . 2 𝐴 ∈ ℋ
2 hvaddlid 31042 . 2 (𝐴 ∈ ℋ → (0 + 𝐴) = 𝐴)
31, 2ax-mp 5 1 (0 + 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2108  (class class class)co 7431  chba 30938   + cva 30939  0c0v 30943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708  ax-hvcom 31020  ax-hv0cl 31022  ax-hvaddid 31023
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729
This theorem is referenced by:  hvsubeq0i  31082  hvaddcani  31084  hsn0elch  31267  hhssnv  31283  shscli  31336
  Copyright terms: Public domain W3C validator