Metamath Proof Explorer


Theorem hial0

Description: A vector whose inner product is always zero is zero. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hial0 AxAihx=0A=0

Proof

Step Hyp Ref Expression
1 oveq2 x=AAihx=AihA
2 1 eqeq1d x=AAihx=0AihA=0
3 2 rspcv AxAihx=0AihA=0
4 his6 AAihA=0A=0
5 3 4 sylibd AxAihx=0A=0
6 oveq1 A=0Aihx=0ihx
7 hi01 x0ihx=0
8 6 7 sylan9eq A=0xAihx=0
9 8 ex A=0xAihx=0
10 9 a1i AA=0xAihx=0
11 10 ralrimdv AA=0xAihx=0
12 5 11 impbid AxAihx=0A=0