Metamath Proof Explorer

Theorem hvaddeq0

Description: If the sum of two vectors is zero, one is the negative of the other. (Contributed by NM, 10-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hvaddeq0 
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) = 0h <-> A = ( -u 1 .h B ) ) )

Proof

Step Hyp Ref Expression
1 hvaddsubval 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) = ( A -h ( -u 1 .h B ) ) )
2 1 eqeq1d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) = 0h <-> ( A -h ( -u 1 .h B ) ) = 0h ) )
3 neg1cn 
 |-  -u 1 e. CC
4 hvmulcl 
 |-  ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h B ) e. ~H )
5 3 4 mpan 
 |-  ( B e. ~H -> ( -u 1 .h B ) e. ~H )
6 hvsubeq0 
 |-  ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H ) -> ( ( A -h ( -u 1 .h B ) ) = 0h <-> A = ( -u 1 .h B ) ) )
7 5 6 sylan2 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A -h ( -u 1 .h B ) ) = 0h <-> A = ( -u 1 .h B ) ) )
8 2 7 bitrd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) = 0h <-> A = ( -u 1 .h B ) ) )