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

Metamath Proof Explorer

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