Theorem hvaddcan

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

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	|- ( A = if ( A e. ~H , A , 0h ) -> ( A +h B ) = ( if ( A e. ~H , A , 0h ) +h B ) )
2		oveq1	|- ( A = if ( A e. ~H , A , 0h ) -> ( A +h C ) = ( if ( A e. ~H , A , 0h ) +h C ) )
3	1 2	eqeq12d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( A +h B ) = ( A +h C ) <-> ( if ( A e. ~H , A , 0h ) +h B ) = ( if ( A e. ~H , A , 0h ) +h C ) ) )
4	3	bibi1d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( ( A +h B ) = ( A +h C ) <-> B = C ) <-> ( ( if ( A e. ~H , A , 0h ) +h B ) = ( if ( A e. ~H , A , 0h ) +h C ) <-> B = C ) ) )
5		oveq2	|- ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) +h B ) = ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) )
6	5	eqeq1d	|- ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. ~H , A , 0h ) +h B ) = ( if ( A e. ~H , A , 0h ) +h C ) <-> ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) = ( if ( A e. ~H , A , 0h ) +h C ) ) )
7		eqeq1	|- ( B = if ( B e. ~H , B , 0h ) -> ( B = C <-> if ( B e. ~H , B , 0h ) = C ) )
8	6 7	bibi12d	|- ( B = if ( B e. ~H , B , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) +h B ) = ( if ( A e. ~H , A , 0h ) +h C ) <-> B = C ) <-> ( ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) = ( if ( A e. ~H , A , 0h ) +h C ) <-> if ( B e. ~H , B , 0h ) = C ) ) )
9		oveq2	|- ( C = if ( C e. ~H , C , 0h ) -> ( if ( A e. ~H , A , 0h ) +h C ) = ( if ( A e. ~H , A , 0h ) +h if ( C e. ~H , C , 0h ) ) )
10	9	eqeq2d	|- ( C = if ( C e. ~H , C , 0h ) -> ( ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) = ( if ( A e. ~H , A , 0h ) +h C ) <-> ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) = ( if ( A e. ~H , A , 0h ) +h if ( C e. ~H , C , 0h ) ) ) )
11		eqeq2	|- ( C = if ( C e. ~H , C , 0h ) -> ( if ( B e. ~H , B , 0h ) = C <-> if ( B e. ~H , B , 0h ) = if ( C e. ~H , C , 0h ) ) )
12	10 11	bibi12d	|- ( C = if ( C e. ~H , C , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) = ( if ( A e. ~H , A , 0h ) +h C ) <-> if ( B e. ~H , B , 0h ) = C ) <-> ( ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) = ( if ( A e. ~H , A , 0h ) +h if ( C e. ~H , C , 0h ) ) <-> if ( B e. ~H , B , 0h ) = if ( C e. ~H , C , 0h ) ) ) )
13		ifhvhv0	|- if ( A e. ~H , A , 0h ) e. ~H
14		ifhvhv0	|- if ( B e. ~H , B , 0h ) e. ~H
15		ifhvhv0	|- if ( C e. ~H , C , 0h ) e. ~H
16	13 14 15	hvaddcani	|- ( ( if ( A e. ~H , A , 0h ) +h if ( B e. ~H , B , 0h ) ) = ( if ( A e. ~H , A , 0h ) +h if ( C e. ~H , C , 0h ) ) <-> if ( B e. ~H , B , 0h ) = if ( C e. ~H , C , 0h ) )
17	4 8 12 16	dedth3h	|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h B ) = ( A +h C ) <-> B = C ) )