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

Metamath Proof Explorer

Theorem hvsubsub4

Description: Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

Ref Expression
Assertion hvsubsub4 
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A -h B ) -h ( C -h D ) ) = ( ( A -h C ) -h ( B -h D ) ) )

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 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A -h B ) -h ( C -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h B ) -h ( C -h D ) ) )
3 oveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A -h C ) = ( if ( A e. ~H , A , 0h ) -h C ) )
4 3 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A -h C ) -h ( B -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h C ) -h ( B -h D ) ) )
5 2 4 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( A -h B ) -h ( C -h D ) ) = ( ( A -h C ) -h ( B -h D ) ) <-> ( ( if ( A e. ~H , A , 0h ) -h B ) -h ( C -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h C ) -h ( B -h D ) ) ) )
6 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 ) ) )
7 6 oveq1d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. ~H , A , 0h ) -h B ) -h ( C -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( C -h D ) ) )
8 oveq1 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( B -h D ) = ( if ( B e. ~H , B , 0h ) -h D ) )
9 8 oveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. ~H , A , 0h ) -h C ) -h ( B -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h C ) -h ( if ( B e. ~H , B , 0h ) -h D ) ) )
10 7 9 eqeq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) -h B ) -h ( C -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h C ) -h ( B -h D ) ) <-> ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( C -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h C ) -h ( if ( B e. ~H , B , 0h ) -h D ) ) ) )
11 oveq1 
 |-  ( C = if ( C e. ~H , C , 0h ) -> ( C -h D ) = ( if ( C e. ~H , C , 0h ) -h D ) )
12 11 oveq2d 
 |-  ( C = if ( C e. ~H , C , 0h ) -> ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( C -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( if ( C e. ~H , C , 0h ) -h D ) ) )
13 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 ) ) )
14 13 oveq1d 
 |-  ( C = if ( C e. ~H , C , 0h ) -> ( ( if ( A e. ~H , A , 0h ) -h C ) -h ( if ( B e. ~H , B , 0h ) -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( C e. ~H , C , 0h ) ) -h ( if ( B e. ~H , B , 0h ) -h D ) ) )
15 12 14 eqeq12d 
 |-  ( C = if ( C e. ~H , C , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( C -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h C ) -h ( if ( B e. ~H , B , 0h ) -h D ) ) <-> ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( if ( C e. ~H , C , 0h ) -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( C e. ~H , C , 0h ) ) -h ( if ( B e. ~H , B , 0h ) -h D ) ) ) )
16 oveq2 
 |-  ( D = if ( D e. ~H , D , 0h ) -> ( if ( C e. ~H , C , 0h ) -h D ) = ( if ( C e. ~H , C , 0h ) -h if ( D e. ~H , D , 0h ) ) )
17 16 oveq2d 
 |-  ( D = if ( D e. ~H , D , 0h ) -> ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( if ( C e. ~H , C , 0h ) -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( if ( C e. ~H , C , 0h ) -h if ( D e. ~H , D , 0h ) ) ) )
18 oveq2 
 |-  ( D = if ( D e. ~H , D , 0h ) -> ( if ( B e. ~H , B , 0h ) -h D ) = ( if ( B e. ~H , B , 0h ) -h if ( D e. ~H , D , 0h ) ) )
19 18 oveq2d 
 |-  ( D = if ( D e. ~H , D , 0h ) -> ( ( if ( A e. ~H , A , 0h ) -h if ( C e. ~H , C , 0h ) ) -h ( if ( B e. ~H , B , 0h ) -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( C e. ~H , C , 0h ) ) -h ( if ( B e. ~H , B , 0h ) -h if ( D e. ~H , D , 0h ) ) ) )
20 17 19 eqeq12d 
 |-  ( D = if ( D e. ~H , D , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( if ( C e. ~H , C , 0h ) -h D ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( C e. ~H , C , 0h ) ) -h ( if ( B e. ~H , B , 0h ) -h D ) ) <-> ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( if ( C e. ~H , C , 0h ) -h if ( D e. ~H , D , 0h ) ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( C e. ~H , C , 0h ) ) -h ( if ( B e. ~H , B , 0h ) -h if ( D e. ~H , D , 0h ) ) ) ) )
21 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
22 ifhvhv0 
 |-  if ( B e. ~H , B , 0h ) e. ~H
23 ifhvhv0 
 |-  if ( C e. ~H , C , 0h ) e. ~H
24 ifhvhv0 
 |-  if ( D e. ~H , D , 0h ) e. ~H
25 21 22 23 24 hvsubsub4i 
 |-  ( ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) -h ( if ( C e. ~H , C , 0h ) -h if ( D e. ~H , D , 0h ) ) ) = ( ( if ( A e. ~H , A , 0h ) -h if ( C e. ~H , C , 0h ) ) -h ( if ( B e. ~H , B , 0h ) -h if ( D e. ~H , D , 0h ) ) )
26 5 10 15 20 25 dedth4h 
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A -h B ) -h ( C -h D ) ) = ( ( A -h C ) -h ( B -h D ) ) )