# 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}\in ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}=0$

### Proof

Step Hyp Ref Expression
1 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
2 ax-hvmul0 ${⊢}{0}_{ℎ}\in ℋ\to 0{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
3 1 2 ax-mp ${⊢}0{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
4 3 oveq1i ${⊢}\left(0{\cdot }_{ℎ}{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{A}={0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}$
5 0cn ${⊢}0\in ℂ$
6 ax-his3 ${⊢}\left(0\in ℂ\wedge {0}_{ℎ}\in ℋ\wedge {A}\in ℋ\right)\to \left(0{\cdot }_{ℎ}{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{A}=0\cdot \left({0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}\right)$
7 5 1 6 mp3an12 ${⊢}{A}\in ℋ\to \left(0{\cdot }_{ℎ}{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{A}=0\cdot \left({0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}\right)$
8 4 7 syl5eqr ${⊢}{A}\in ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}=0\cdot \left({0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}\right)$
9 hicl ${⊢}\left({0}_{ℎ}\in ℋ\wedge {A}\in ℋ\right)\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
10 1 9 mpan ${⊢}{A}\in ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
11 10 mul02d ${⊢}{A}\in ℋ\to 0\cdot \left({0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}\right)=0$
12 8 11 eqtrd ${⊢}{A}\in ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}=0$