# 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
`|- ( A e. ~H -> ( A. x e. ~H ( A .ih x ) = 0 <-> A = 0h ) )`

### Proof

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