# Metamath Proof Explorer

## Theorem hial02

Description: A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion hial02
`|- ( A e. ~H -> ( A. x e. ~H ( x .ih A ) = 0 <-> A = 0h ) )`

### Proof

Step Hyp Ref Expression
1 oveq1
` |-  ( x = A -> ( x .ih A ) = ( A .ih A ) )`
2 1 eqeq1d
` |-  ( x = A -> ( ( x .ih A ) = 0 <-> ( A .ih A ) = 0 ) )`
3 2 rspcv
` |-  ( A e. ~H -> ( A. x e. ~H ( x .ih A ) = 0 -> ( A .ih A ) = 0 ) )`
4 his6
` |-  ( A e. ~H -> ( ( A .ih A ) = 0 <-> A = 0h ) )`
5 3 4 sylibd
` |-  ( A e. ~H -> ( A. x e. ~H ( x .ih A ) = 0 -> A = 0h ) )`
6 oveq2
` |-  ( A = 0h -> ( x .ih A ) = ( x .ih 0h ) )`
7 hi02
` |-  ( x e. ~H -> ( x .ih 0h ) = 0 )`
8 6 7 sylan9eq
` |-  ( ( A = 0h /\ x e. ~H ) -> ( x .ih A ) = 0 )`
9 8 ex
` |-  ( A = 0h -> ( x e. ~H -> ( x .ih A ) = 0 ) )`
10 9 a1i
` |-  ( A e. ~H -> ( A = 0h -> ( x e. ~H -> ( x .ih A ) = 0 ) ) )`
11 10 ralrimdv
` |-  ( A e. ~H -> ( A = 0h -> A. x e. ~H ( x .ih A ) = 0 ) )`
12 5 11 impbid
` |-  ( A e. ~H -> ( A. x e. ~H ( x .ih A ) = 0 <-> A = 0h ) )`