Theorem hv2times

Description: Two times a vector. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-2	|- 2 = ( 1 + 1 )
2	1	oveq1i	|- ( 2 .h A ) = ( ( 1 + 1 ) .h A )
3		ax-1cn	|- 1 e. CC
4		ax-hvdistr2	|- ( ( 1 e. CC /\ 1 e. CC /\ A e. ~H ) -> ( ( 1 + 1 ) .h A ) = ( ( 1 .h A ) +h ( 1 .h A ) ) )
5	3 3 4	mp3an12	|- ( A e. ~H -> ( ( 1 + 1 ) .h A ) = ( ( 1 .h A ) +h ( 1 .h A ) ) )
6	2 5	eqtrid	|- ( A e. ~H -> ( 2 .h A ) = ( ( 1 .h A ) +h ( 1 .h A ) ) )
7		ax-hvdistr1	|- ( ( 1 e. CC /\ A e. ~H /\ A e. ~H ) -> ( 1 .h ( A +h A ) ) = ( ( 1 .h A ) +h ( 1 .h A ) ) )
8	3 7	mp3an1	|- ( ( A e. ~H /\ A e. ~H ) -> ( 1 .h ( A +h A ) ) = ( ( 1 .h A ) +h ( 1 .h A ) ) )
9	8	anidms	|- ( A e. ~H -> ( 1 .h ( A +h A ) ) = ( ( 1 .h A ) +h ( 1 .h A ) ) )
10		hvaddcl	|- ( ( A e. ~H /\ A e. ~H ) -> ( A +h A ) e. ~H )
11	10	anidms	|- ( A e. ~H -> ( A +h A ) e. ~H )
12		ax-hvmulid	|- ( ( A +h A ) e. ~H -> ( 1 .h ( A +h A ) ) = ( A +h A ) )
13	11 12	syl	|- ( A e. ~H -> ( 1 .h ( A +h A ) ) = ( A +h A ) )
14	6 9 13	3eqtr2d	|- ( A e. ~H -> ( 2 .h A ) = ( A +h A ) )