Theorem hvaddcan2

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

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

Proof

Step	Hyp	Ref	Expression
1		ax-hvcom	|- ( ( C e. ~H /\ A e. ~H ) -> ( C +h A ) = ( A +h C ) )
2	1	3adant3	|- ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( C +h A ) = ( A +h C ) )
3		ax-hvcom	|- ( ( C e. ~H /\ B e. ~H ) -> ( C +h B ) = ( B +h C ) )
4	3	3adant2	|- ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( C +h B ) = ( B +h C ) )
5	2 4	eqeq12d	|- ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( ( C +h A ) = ( C +h B ) <-> ( A +h C ) = ( B +h C ) ) )
6		hvaddcan	|- ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( ( C +h A ) = ( C +h B ) <-> A = B ) )
7	5 6	bitr3d	|- ( ( C e. ~H /\ A e. ~H /\ B e. ~H ) -> ( ( A +h C ) = ( B +h C ) <-> A = B ) )
8	7	3coml	|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h C ) = ( B +h C ) <-> A = B ) )