Metamath Proof Explorer

Theorem hial2eq2

Description: Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax-his1 
 |-  ( ( A e. ~H /\ x e. ~H ) -> ( A .ih x ) = ( * ` ( x .ih A ) ) )
2 ax-his1 
 |-  ( ( B e. ~H /\ x e. ~H ) -> ( B .ih x ) = ( * ` ( x .ih B ) ) )
3 1 2 eqeqan12d 
 |-  ( ( ( A e. ~H /\ x e. ~H ) /\ ( B e. ~H /\ x e. ~H ) ) -> ( ( A .ih x ) = ( B .ih x ) <-> ( * ` ( x .ih A ) ) = ( * ` ( x .ih B ) ) ) )
4 hicl 
 |-  ( ( x e. ~H /\ A e. ~H ) -> ( x .ih A ) e. CC )
5 4 ancoms 
 |-  ( ( A e. ~H /\ x e. ~H ) -> ( x .ih A ) e. CC )
6 hicl 
 |-  ( ( x e. ~H /\ B e. ~H ) -> ( x .ih B ) e. CC )
7 6 ancoms 
 |-  ( ( B e. ~H /\ x e. ~H ) -> ( x .ih B ) e. CC )
8 cj11 
 |-  ( ( ( x .ih A ) e. CC /\ ( x .ih B ) e. CC ) -> ( ( * ` ( x .ih A ) ) = ( * ` ( x .ih B ) ) <-> ( x .ih A ) = ( x .ih B ) ) )
9 5 7 8 syl2an 
 |-  ( ( ( A e. ~H /\ x e. ~H ) /\ ( B e. ~H /\ x e. ~H ) ) -> ( ( * ` ( x .ih A ) ) = ( * ` ( x .ih B ) ) <-> ( x .ih A ) = ( x .ih B ) ) )
10 3 9 bitr2d 
 |-  ( ( ( A e. ~H /\ x e. ~H ) /\ ( B e. ~H /\ x e. ~H ) ) -> ( ( x .ih A ) = ( x .ih B ) <-> ( A .ih x ) = ( B .ih x ) ) )
11 10 anandirs 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ~H ) -> ( ( x .ih A ) = ( x .ih B ) <-> ( A .ih x ) = ( B .ih x ) ) )
12 11 ralbidva 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( x .ih A ) = ( x .ih B ) <-> A. x e. ~H ( A .ih x ) = ( B .ih x ) ) )
13 hial2eq 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( A .ih x ) = ( B .ih x ) <-> A = B ) )
14 12 13 bitrd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A. x e. ~H ( x .ih A ) = ( x .ih B ) <-> A = B ) )