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

Metamath Proof Explorer

Theorem hvsubcan

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

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

Proof

Step Hyp Ref Expression
1 hvsubval 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
2 1 3adant3 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
3 hvsubval 
 |-  ( ( A e. ~H /\ C e. ~H ) -> ( A -h C ) = ( A +h ( -u 1 .h C ) ) )
4 3 3adant2 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A -h C ) = ( A +h ( -u 1 .h C ) ) )
5 2 4 eqeq12d 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) = ( A -h C ) <-> ( A +h ( -u 1 .h B ) ) = ( A +h ( -u 1 .h C ) ) ) )
6 neg1cn 
 |-  -u 1 e. CC
7 hvmulcl 
 |-  ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h B ) e. ~H )
8 6 7 mpan 
 |-  ( B e. ~H -> ( -u 1 .h B ) e. ~H )
9 hvmulcl 
 |-  ( ( -u 1 e. CC /\ C e. ~H ) -> ( -u 1 .h C ) e. ~H )
10 6 9 mpan 
 |-  ( C e. ~H -> ( -u 1 .h C ) e. ~H )
11 hvaddcan 
 |-  ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H /\ ( -u 1 .h C ) e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) = ( A +h ( -u 1 .h C ) ) <-> ( -u 1 .h B ) = ( -u 1 .h C ) ) )
12 10 11 syl3an3 
 |-  ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) = ( A +h ( -u 1 .h C ) ) <-> ( -u 1 .h B ) = ( -u 1 .h C ) ) )
13 8 12 syl3an2 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) = ( A +h ( -u 1 .h C ) ) <-> ( -u 1 .h B ) = ( -u 1 .h C ) ) )
14 neg1ne0 
 |-  -u 1 =/= 0
15 6 14 pm3.2i 
 |-  ( -u 1 e. CC /\ -u 1 =/= 0 )
16 hvmulcan 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) = ( -u 1 .h C ) <-> B = C ) )
17 15 16 mp3an1 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) = ( -u 1 .h C ) <-> B = C ) )
18 17 3adant1 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) = ( -u 1 .h C ) <-> B = C ) )
19 5 13 18 3bitrd 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) = ( A -h C ) <-> B = C ) )