Theorem hvsubadd

Description: Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

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

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	1	eqeq1d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( A -h B ) = C <-> ( if ( A e. ~H , A , 0h ) -h B ) = C ) )
3		eqeq2	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( B +h C ) = A <-> ( B +h C ) = if ( A e. ~H , A , 0h ) ) )
4	2 3	bibi12d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( ( A -h B ) = C <-> ( B +h C ) = A ) <-> ( ( if ( A e. ~H , A , 0h ) -h B ) = C <-> ( B +h C ) = if ( A e. ~H , A , 0h ) ) ) )
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 ) = C <-> ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) = C ) )
7		oveq1	|- ( B = if ( B e. ~H , B , 0h ) -> ( B +h C ) = ( if ( B e. ~H , B , 0h ) +h C ) )
8	7	eqeq1d	|- ( B = if ( B e. ~H , B , 0h ) -> ( ( B +h C ) = if ( A e. ~H , A , 0h ) <-> ( if ( B e. ~H , B , 0h ) +h C ) = if ( A e. ~H , A , 0h ) ) )
9	6 8	bibi12d	|- ( B = if ( B e. ~H , B , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) -h B ) = C <-> ( B +h C ) = if ( A e. ~H , A , 0h ) ) <-> ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) = C <-> ( if ( B e. ~H , B , 0h ) +h C ) = if ( A e. ~H , A , 0h ) ) ) )
10		eqeq2	|- ( C = if ( C e. ~H , C , 0h ) -> ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) = C <-> ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) = if ( C e. ~H , C , 0h ) ) )
11		oveq2	|- ( C = if ( C e. ~H , C , 0h ) -> ( if ( B e. ~H , B , 0h ) +h C ) = ( if ( B e. ~H , B , 0h ) +h if ( C e. ~H , C , 0h ) ) )
12	11	eqeq1d	|- ( C = if ( C e. ~H , C , 0h ) -> ( ( if ( B e. ~H , B , 0h ) +h C ) = if ( A e. ~H , A , 0h ) <-> ( if ( B e. ~H , B , 0h ) +h if ( C e. ~H , C , 0h ) ) = if ( A e. ~H , A , 0h ) ) )
13	10 12	bibi12d	|- ( C = if ( C e. ~H , C , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) = C <-> ( if ( B e. ~H , B , 0h ) +h C ) = if ( A e. ~H , A , 0h ) ) <-> ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) = if ( C e. ~H , C , 0h ) <-> ( if ( B e. ~H , B , 0h ) +h if ( C e. ~H , C , 0h ) ) = if ( A e. ~H , A , 0h ) ) ) )
14		ifhvhv0	|- if ( A e. ~H , A , 0h ) e. ~H
15		ifhvhv0	|- if ( B e. ~H , B , 0h ) e. ~H
16		ifhvhv0	|- if ( C e. ~H , C , 0h ) e. ~H
17	14 15 16	hvsubaddi	|- ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) = if ( C e. ~H , C , 0h ) <-> ( if ( B e. ~H , B , 0h ) +h if ( C e. ~H , C , 0h ) ) = if ( A e. ~H , A , 0h ) )
18	4 9 13 17	dedth3h	|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) = C <-> ( B +h C ) = A ) )