Metamath Proof Explorer

Theorem hosubcl

Description: Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hosubcl 
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) : ~H --> ~H )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( S -op T ) = ( if ( S : ~H --> ~H , S , 0hop ) -op T ) )
2 1 feq1d 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( ( S -op T ) : ~H --> ~H <-> ( if ( S : ~H --> ~H , S , 0hop ) -op T ) : ~H --> ~H ) )
3 oveq2 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( if ( S : ~H --> ~H , S , 0hop ) -op T ) = ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) )
4 3 feq1d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( ( if ( S : ~H --> ~H , S , 0hop ) -op T ) : ~H --> ~H <-> ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) : ~H --> ~H ) )
5 ho0f 
 |-  0hop : ~H --> ~H
6 5 elimf 
 |-  if ( S : ~H --> ~H , S , 0hop ) : ~H --> ~H
7 5 elimf 
 |-  if ( T : ~H --> ~H , T , 0hop ) : ~H --> ~H
8 6 7 hosubcli 
 |-  ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) : ~H --> ~H
9 2 4 8 dedth2h 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) : ~H --> ~H )