Metamath Proof Explorer


Theorem hvaddlidi

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

Ref Expression
Hypothesis hvaddlid.1 𝐴 ∈ ℋ
Assertion hvaddlidi ( 0 + 𝐴 ) = 𝐴

Proof

Step Hyp Ref Expression
1 hvaddlid.1 𝐴 ∈ ℋ
2 hvaddlid ( 𝐴 ∈ ℋ → ( 0 + 𝐴 ) = 𝐴 )
3 1 2 ax-mp ( 0 + 𝐴 ) = 𝐴