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 AAih0=0

Proof

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