Metamath Proof Explorer

Axiom ax-hvaddid

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

Ref Expression
Assertion ax-hvaddid 
|- ( A e. ~H -> ( A +h 0h ) = A )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 chba 
 |-  ~H
2 0 1 wcel 
 |-  A e. ~H
3 cva 
 |-  +h
4 c0v 
 |-  0h
5 0 4 3 co 
 |-  ( A +h 0h )
6 5 0 wceq 
 |-  ( A +h 0h ) = A
7 2 6 wi 
 |-  ( A e. ~H -> ( A +h 0h ) = A )