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

Metamath Proof Explorer

Theorem hial2eq

Description: Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion hial2eq 
|- ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( A .ih x ) = ( B .ih x ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 hvsubcl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) e. ~H )
2 oveq2 
 |-  ( x = ( A -h B ) -> ( A .ih x ) = ( A .ih ( A -h B ) ) )
3 oveq2 
 |-  ( x = ( A -h B ) -> ( B .ih x ) = ( B .ih ( A -h B ) ) )
4 2 3 eqeq12d 
 |-  ( x = ( A -h B ) -> ( ( A .ih x ) = ( B .ih x ) <-> ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) ) )
5 4 rspcv 
 |-  ( ( A -h B ) e. ~H -> ( A. x e. ~H ( A .ih x ) = ( B .ih x ) -> ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) ) )
6 1 5 syl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( A .ih x ) = ( B .ih x ) -> ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) ) )
7 hi2eq 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) <-> A = B ) )
8 6 7 sylibd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( A .ih x ) = ( B .ih x ) -> A = B ) )
9 oveq1 
 |-  ( A = B -> ( A .ih x ) = ( B .ih x ) )
10 9 ralrimivw 
 |-  ( A = B -> A. x e. ~H ( A .ih x ) = ( B .ih x ) )
11 8 10 impbid1 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( A .ih x ) = ( B .ih x ) <-> A = B ) )