Metamath Proof Explorer

Theorem hvaddid2

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

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

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 ax-hvcom 
 |-  ( ( A e. ~H /\ 0h e. ~H ) -> ( A +h 0h ) = ( 0h +h A ) )
3 1 2 mpan2 
 |-  ( A e. ~H -> ( A +h 0h ) = ( 0h +h A ) )
4 ax-hvaddid 
 |-  ( A e. ~H -> ( A +h 0h ) = A )
5 3 4 eqtr3d 
 |-  ( A e. ~H -> ( 0h +h A ) = A )