Metamath Proof Explorer


Theorem hi02

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

Ref Expression
Assertion hi02 A A ih 0 = 0

Proof

Step Hyp Ref Expression
1 ax-hv0cl 0
2 ax-his1 A 0 A ih 0 = 0 ih A
3 1 2 mpan2 A A ih 0 = 0 ih A
4 hi01 A 0 ih A = 0
5 4 fveq2d A 0 ih A = 0
6 cj0 0 = 0
7 5 6 eqtrdi A 0 ih A = 0
8 3 7 eqtrd A A ih 0 = 0