Metamath Proof Explorer

Theorem hoaddcom

Description: Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

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 oveq2 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( T +op S ) = ( T +op if ( S : ~H --> ~H , S , 0hop ) ) )
3 1 2 eqeq12d 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( ( S +op T ) = ( T +op S ) <-> ( if ( S : ~H --> ~H , S , 0hop ) +op T ) = ( T +op if ( S : ~H --> ~H , S , 0hop ) ) ) )
4 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 ) ) )
5 oveq1 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( T +op if ( S : ~H --> ~H , S , 0hop ) ) = ( if ( T : ~H --> ~H , T , 0hop ) +op if ( S : ~H --> ~H , S , 0hop ) ) )
6 4 5 eqeq12d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( ( if ( S : ~H --> ~H , S , 0hop ) +op T ) = ( T +op if ( S : ~H --> ~H , S , 0hop ) ) <-> ( if ( S : ~H --> ~H , S , 0hop ) +op if ( T : ~H --> ~H , T , 0hop ) ) = ( if ( T : ~H --> ~H , T , 0hop ) +op if ( S : ~H --> ~H , S , 0hop ) ) ) )
7 ho0f 
 |-  0hop : ~H --> ~H
8 7 elimf 
 |-  if ( S : ~H --> ~H , S , 0hop ) : ~H --> ~H
9 7 elimf 
 |-  if ( T : ~H --> ~H , T , 0hop ) : ~H --> ~H
10 8 9 hoaddcomi 
 |-  ( if ( S : ~H --> ~H , S , 0hop ) +op if ( T : ~H --> ~H , T , 0hop ) ) = ( if ( T : ~H --> ~H , T , 0hop ) +op if ( S : ~H --> ~H , S , 0hop ) )
11 3 6 10 dedth2h 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) = ( T +op S ) )