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

Theorem hvaddlidi 31057
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 31051 . 2 (𝐴 ∈ ℋ → (0 + 𝐴) = 𝐴)
31, 2ax-mp 5 1 (0 + 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1536  wcel 2105  (class class class)co 7430  chba 30947   + cva 30948  0c0v 30952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705  ax-hvcom 31029  ax-hv0cl 31031  ax-hvaddid 31032
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726
This theorem is referenced by:  hvsubeq0i  31091  hvaddcani  31093  hsn0elch  31276  hhssnv  31292  shscli  31345
  Copyright terms: Public domain W3C validator