Theorem hv2times

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

	Ref	Expression
Assertion	hv2times	⊢ ( 𝐴 ∈ ℋ → ( 2 ·ℎ 𝐴 ) = ( 𝐴 +ℎ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-2	⊢ 2 = ( 1 + 1 )
2	1	oveq1i	⊢ ( 2 ·ℎ 𝐴 ) = ( ( 1 + 1 ) ·ℎ 𝐴 )
3		ax-1cn	⊢ 1 ∈ ℂ
4		ax-hvdistr2	⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( 1 + 1 ) ·ℎ 𝐴 ) = ( ( 1 ·ℎ 𝐴 ) +ℎ ( 1 ·ℎ 𝐴 ) ) )
5	3 3 4	mp3an12	⊢ ( 𝐴 ∈ ℋ → ( ( 1 + 1 ) ·ℎ 𝐴 ) = ( ( 1 ·ℎ 𝐴 ) +ℎ ( 1 ·ℎ 𝐴 ) ) )
6	2 5	eqtrid	⊢ ( 𝐴 ∈ ℋ → ( 2 ·ℎ 𝐴 ) = ( ( 1 ·ℎ 𝐴 ) +ℎ ( 1 ·ℎ 𝐴 ) ) )
7		ax-hvdistr1	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 1 ·ℎ ( 𝐴 +ℎ 𝐴 ) ) = ( ( 1 ·ℎ 𝐴 ) +ℎ ( 1 ·ℎ 𝐴 ) ) )
8	3 7	mp3an1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 1 ·ℎ ( 𝐴 +ℎ 𝐴 ) ) = ( ( 1 ·ℎ 𝐴 ) +ℎ ( 1 ·ℎ 𝐴 ) ) )
9	8	anidms	⊢ ( 𝐴 ∈ ℋ → ( 1 ·ℎ ( 𝐴 +ℎ 𝐴 ) ) = ( ( 1 ·ℎ 𝐴 ) +ℎ ( 1 ·ℎ 𝐴 ) ) )
10		hvaddcl	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 +ℎ 𝐴 ) ∈ ℋ )
11	10	anidms	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 +ℎ 𝐴 ) ∈ ℋ )
12		ax-hvmulid	⊢ ( ( 𝐴 +ℎ 𝐴 ) ∈ ℋ → ( 1 ·ℎ ( 𝐴 +ℎ 𝐴 ) ) = ( 𝐴 +ℎ 𝐴 ) )
13	11 12	syl	⊢ ( 𝐴 ∈ ℋ → ( 1 ·ℎ ( 𝐴 +ℎ 𝐴 ) ) = ( 𝐴 +ℎ 𝐴 ) )
14	6 9 13	3eqtr2d	⊢ ( 𝐴 ∈ ℋ → ( 2 ·ℎ 𝐴 ) = ( 𝐴 +ℎ 𝐴 ) )