Metamath Proof Explorer


Theorem hi01

Description: Inner product with the 0 vector. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hi01 ( 𝐴 ∈ ℋ → ( 0 ·ih 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 ax-hv0cl 0 ∈ ℋ
2 ax-hvmul0 ( 0 ∈ ℋ → ( 0 · 0 ) = 0 )
3 1 2 ax-mp ( 0 · 0 ) = 0
4 3 oveq1i ( ( 0 · 0 ) ·ih 𝐴 ) = ( 0 ·ih 𝐴 )
5 0cn 0 ∈ ℂ
6 ax-his3 ( ( 0 ∈ ℂ ∧ 0 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 0 · 0 ) ·ih 𝐴 ) = ( 0 · ( 0 ·ih 𝐴 ) ) )
7 5 1 6 mp3an12 ( 𝐴 ∈ ℋ → ( ( 0 · 0 ) ·ih 𝐴 ) = ( 0 · ( 0 ·ih 𝐴 ) ) )
8 4 7 eqtr3id ( 𝐴 ∈ ℋ → ( 0 ·ih 𝐴 ) = ( 0 · ( 0 ·ih 𝐴 ) ) )
9 hicl ( ( 0 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 0 ·ih 𝐴 ) ∈ ℂ )
10 1 9 mpan ( 𝐴 ∈ ℋ → ( 0 ·ih 𝐴 ) ∈ ℂ )
11 10 mul02d ( 𝐴 ∈ ℋ → ( 0 · ( 0 ·ih 𝐴 ) ) = 0 )
12 8 11 eqtrd ( 𝐴 ∈ ℋ → ( 0 ·ih 𝐴 ) = 0 )