This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )