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