This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )