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 ⊢ A ∈ ℋ → 0 ℎ ⋅ ih A = 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 A = 0 ℎ ⋅ ih A
5 0cn ⊢ 0 ∈ ℂ
6 ax-his3 ⊢ 0 ∈ ℂ ∧ 0 ℎ ∈ ℋ ∧ A ∈ ℋ → 0 ⋅ ℎ 0 ℎ ⋅ ih A = 0 ⋅ 0 ℎ ⋅ ih A
7 5 1 6 mp3an12 ⊢ A ∈ ℋ → 0 ⋅ ℎ 0 ℎ ⋅ ih A = 0 ⋅ 0 ℎ ⋅ ih A
8 4 7 eqtr3id ⊢ A ∈ ℋ → 0 ℎ ⋅ ih A = 0 ⋅ 0 ℎ ⋅ ih A
9 hicl ⊢ 0 ℎ ∈ ℋ ∧ A ∈ ℋ → 0 ℎ ⋅ ih A ∈ ℂ
10 1 9 mpan ⊢ A ∈ ℋ → 0 ℎ ⋅ ih A ∈ ℂ
11 10 mul02d ⊢ A ∈ ℋ → 0 ⋅ 0 ℎ ⋅ ih A = 0
12 8 11 eqtrd ⊢ A ∈ ℋ → 0 ℎ ⋅ ih A = 0