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

Metamath Proof Explorer

Theorem honegsub

Description: Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion honegsub 
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op U ) ) = ( T -op U ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( T +op ( -u 1 .op U ) ) = ( if ( T : ~H --> ~H , T , 0hop ) +op ( -u 1 .op U ) ) )
2 oveq1 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( T -op U ) = ( if ( T : ~H --> ~H , T , 0hop ) -op U ) )
3 1 2 eqeq12d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( ( T +op ( -u 1 .op U ) ) = ( T -op U ) <-> ( if ( T : ~H --> ~H , T , 0hop ) +op ( -u 1 .op U ) ) = ( if ( T : ~H --> ~H , T , 0hop ) -op U ) ) )
4 oveq2 
 |-  ( U = if ( U : ~H --> ~H , U , 0hop ) -> ( -u 1 .op U ) = ( -u 1 .op if ( U : ~H --> ~H , U , 0hop ) ) )
5 4 oveq2d 
 |-  ( U = if ( U : ~H --> ~H , U , 0hop ) -> ( if ( T : ~H --> ~H , T , 0hop ) +op ( -u 1 .op U ) ) = ( if ( T : ~H --> ~H , T , 0hop ) +op ( -u 1 .op if ( U : ~H --> ~H , U , 0hop ) ) ) )
6 oveq2 
 |-  ( U = if ( U : ~H --> ~H , U , 0hop ) -> ( if ( T : ~H --> ~H , T , 0hop ) -op U ) = ( if ( T : ~H --> ~H , T , 0hop ) -op if ( U : ~H --> ~H , U , 0hop ) ) )
7 5 6 eqeq12d 
 |-  ( U = if ( U : ~H --> ~H , U , 0hop ) -> ( ( if ( T : ~H --> ~H , T , 0hop ) +op ( -u 1 .op U ) ) = ( if ( T : ~H --> ~H , T , 0hop ) -op U ) <-> ( if ( T : ~H --> ~H , T , 0hop ) +op ( -u 1 .op if ( U : ~H --> ~H , U , 0hop ) ) ) = ( if ( T : ~H --> ~H , T , 0hop ) -op if ( U : ~H --> ~H , U , 0hop ) ) ) )
8 ho0f 
 |-  0hop : ~H --> ~H
9 8 elimf 
 |-  if ( T : ~H --> ~H , T , 0hop ) : ~H --> ~H
10 8 elimf 
 |-  if ( U : ~H --> ~H , U , 0hop ) : ~H --> ~H
11 9 10 honegsubi 
 |-  ( if ( T : ~H --> ~H , T , 0hop ) +op ( -u 1 .op if ( U : ~H --> ~H , U , 0hop ) ) ) = ( if ( T : ~H --> ~H , T , 0hop ) -op if ( U : ~H --> ~H , U , 0hop ) )
12 3 7 11 dedth2h 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op U ) ) = ( T -op U ) )