Metamath Proof Explorer

Theorem hvmul0

Description: Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hvmul0 ( 𝐴 ∈ ℂ → ( 𝐴 ·ℎ 0ℎ ) = 0ℎ )

Proof

Step Hyp Ref Expression
1 mul01 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 )
2 1 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 · 0 ) ·ℎ 0ℎ ) = ( 0 ·ℎ 0ℎ ) )
3 ax-hv0cl ⊢ 0ℎ ∈ ℋ
4 ax-hvmul0 ⊢ ( 0ℎ ∈ ℋ → ( 0 ·ℎ 0ℎ ) = 0ℎ )
5 3 4 ax-mp ⊢ ( 0 ·ℎ 0ℎ ) = 0ℎ
6 2 5 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 · 0 ) ·ℎ 0ℎ ) = 0ℎ )
7 0cn ⊢ 0 ∈ ℂ
8 ax-hvmulass ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ∧ 0ℎ ∈ ℋ ) → ( ( 𝐴 · 0 ) ·ℎ 0ℎ ) = ( 𝐴 ·ℎ ( 0 ·ℎ 0ℎ ) ) )
9 7 3 8 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 · 0 ) ·ℎ 0ℎ ) = ( 𝐴 ·ℎ ( 0 ·ℎ 0ℎ ) ) )
10 6 9 eqtr3d ⊢ ( 𝐴 ∈ ℂ → 0ℎ = ( 𝐴 ·ℎ ( 0 ·ℎ 0ℎ ) ) )
11 5 oveq2i ⊢ ( 𝐴 ·ℎ ( 0 ·ℎ 0ℎ ) ) = ( 𝐴 ·ℎ 0ℎ )
12 10 11 eqtr2di ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ·ℎ 0ℎ ) = 0ℎ )