Metamath Proof Explorer

Theorem hi2eq

Description: Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvsubcl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) e. ~H )
2 his2sub 
 |-  ( ( A e. ~H /\ B e. ~H /\ ( A -h B ) e. ~H ) -> ( ( A -h B ) .ih ( A -h B ) ) = ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) )
3 1 2 mpd3an3 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A -h B ) .ih ( A -h B ) ) = ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) )
4 3 eqeq1d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A -h B ) .ih ( A -h B ) ) = 0 <-> ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) = 0 ) )
5 his6 
 |-  ( ( A -h B ) e. ~H -> ( ( ( A -h B ) .ih ( A -h B ) ) = 0 <-> ( A -h B ) = 0h ) )
6 1 5 syl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A -h B ) .ih ( A -h B ) ) = 0 <-> ( A -h B ) = 0h ) )
7 4 6 bitr3d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) = 0 <-> ( A -h B ) = 0h ) )
8 hicl 
 |-  ( ( A e. ~H /\ ( A -h B ) e. ~H ) -> ( A .ih ( A -h B ) ) e. CC )
9 1 8 syldan 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih ( A -h B ) ) e. CC )
10 simpr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> B e. ~H )
11 hicl 
 |-  ( ( B e. ~H /\ ( A -h B ) e. ~H ) -> ( B .ih ( A -h B ) ) e. CC )
12 10 1 11 syl2anc 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( B .ih ( A -h B ) ) e. CC )
13 9 12 subeq0ad 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) = 0 <-> ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) ) )
14 hvsubeq0 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A -h B ) = 0h <-> A = B ) )
15 7 13 14 3bitr3d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) <-> A = B ) )