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

Metamath Proof Explorer

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