Metamath Proof Explorer

Theorem hvsubcan2

Description: Cancellation law for vector addition. (Contributed by NM, 18-May-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvsubcl 
 |-  ( ( C e. ~H /\ A e. ~H ) -> ( C -h A ) e. ~H )
2 1 3adant3 
 |-  ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( C -h A ) e. ~H )
3 hvsubcl 
 |-  ( ( C e. ~H /\ B e. ~H ) -> ( C -h B ) e. ~H )
4 3 3adant2 
 |-  ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( C -h B ) e. ~H )
5 neg1cn 
 |-  -u 1 e. CC
6 neg1ne0 
 |-  -u 1 =/= 0
7 5 6 pm3.2i 
 |-  ( -u 1 e. CC /\ -u 1 =/= 0 )
8 hvmulcan 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( C -h A ) e. ~H /\ ( C -h B ) e. ~H ) -> ( ( -u 1 .h ( C -h A ) ) = ( -u 1 .h ( C -h B ) ) <-> ( C -h A ) = ( C -h B ) ) )
9 7 8 mp3an1 
 |-  ( ( ( C -h A ) e. ~H /\ ( C -h B ) e. ~H ) -> ( ( -u 1 .h ( C -h A ) ) = ( -u 1 .h ( C -h B ) ) <-> ( C -h A ) = ( C -h B ) ) )
10 2 4 9 syl2anc 
 |-  ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( ( -u 1 .h ( C -h A ) ) = ( -u 1 .h ( C -h B ) ) <-> ( C -h A ) = ( C -h B ) ) )
11 hvnegdi 
 |-  ( ( C e. ~H /\ A e. ~H ) -> ( -u 1 .h ( C -h A ) ) = ( A -h C ) )
12 11 3adant3 
 |-  ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( -u 1 .h ( C -h A ) ) = ( A -h C ) )
13 hvnegdi 
 |-  ( ( C e. ~H /\ B e. ~H ) -> ( -u 1 .h ( C -h B ) ) = ( B -h C ) )
14 13 3adant2 
 |-  ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( -u 1 .h ( C -h B ) ) = ( B -h C ) )
15 12 14 eqeq12d 
 |-  ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( ( -u 1 .h ( C -h A ) ) = ( -u 1 .h ( C -h B ) ) <-> ( A -h C ) = ( B -h C ) ) )
16 hvsubcan 
 |-  ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( ( C -h A ) = ( C -h B ) <-> A = B ) )
17 10 15 16 3bitr3d 
 |-  ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( ( A -h C ) = ( B -h C ) <-> A = B ) )
18 17 3coml 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h C ) = ( B -h C ) <-> A = B ) )