Theorem hvaddlid 31312

Description: Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
hvaddlid	⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴)

Proof of Theorem hvaddlid

Step	Hyp	Ref	Expression
1		ax-hv0cl 31292	. . 3 ⊢ 0ℎ ∈ ℋ
2		ax-hvcom 31290	. . 3 ⊢ ((𝐴 ∈ ℋ ∧ 0ℎ ∈ ℋ) → (𝐴 +ℎ 0ℎ) = (0ℎ +ℎ 𝐴))
3	1, 2	mpan2 703	. 2 ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = (0ℎ +ℎ 𝐴))
4		ax-hvaddid 31293	. 2 ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)
5	3, 4	eqtr3d 2806	1 ⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  (class class class)co 7408   ℋchba 31208   +_ℎ cva 31209  0_ℎc0v 31213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741  ax-hvcom 31290  ax-hv0cl 31292  ax-hvaddid 31293

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  hv2neg  31317  hvaddlidi  31318  hvaddsub4  31367  hilablo  31449  hilid  31450  shunssi  31657  spanunsni  31868  5oalem2  31944  3oalem2  31952