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