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