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

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