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		hvaddid2	|- ( ( -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 ) )