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