This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hv2neg

Description: Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hv2neg 
|- ( A e. ~H -> ( 0h -h A ) = ( -u 1 .h A ) )

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 hvsubval 
 |-  ( ( 0h e. ~H /\ A e. ~H ) -> ( 0h -h A ) = ( 0h +h ( -u 1 .h A ) ) )
3 1 2 mpan 
 |-  ( A e. ~H -> ( 0h -h A ) = ( 0h +h ( -u 1 .h A ) ) )
4 neg1cn 
 |-  -u 1 e. CC
5 hvmulcl 
 |-  ( ( -u 1 e. CC /\ A e. ~H ) -> ( -u 1 .h A ) e. ~H )
6 4 5 mpan 
 |-  ( A e. ~H -> ( -u 1 .h A ) e. ~H )
7 hvaddlid 
 |-  ( ( -u 1 .h A ) e. ~H -> ( 0h +h ( -u 1 .h A ) ) = ( -u 1 .h A ) )
8 6 7 syl 
 |-  ( A e. ~H -> ( 0h +h ( -u 1 .h A ) ) = ( -u 1 .h A ) )
9 3 8 eqtrd 
 |-  ( A e. ~H -> ( 0h -h A ) = ( -u 1 .h A ) )