Metamath Proof Explorer

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 syl5eq ⊢ ( 𝐴 ∈ ℋ → ( 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 ·ℎ 𝐴 ) = ( 𝐴 +ℎ 𝐴 ) )