Metamath Proof Explorer

Theorem hoddi

Description: Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri does not require linearity.) (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoddi 
|- ( ( R e. LinOp /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) ) )

Proof

Step Hyp Ref Expression
1 coeq1 
 |-  ( R = if ( R e. LinOp , R , 0hop ) -> ( R o. ( S -op T ) ) = ( if ( R e. LinOp , R , 0hop ) o. ( S -op T ) ) )
2 coeq1 
 |-  ( R = if ( R e. LinOp , R , 0hop ) -> ( R o. S ) = ( if ( R e. LinOp , R , 0hop ) o. S ) )
3 coeq1 
 |-  ( R = if ( R e. LinOp , R , 0hop ) -> ( R o. T ) = ( if ( R e. LinOp , R , 0hop ) o. T ) )
4 2 3 oveq12d 
 |-  ( R = if ( R e. LinOp , R , 0hop ) -> ( ( R o. S ) -op ( R o. T ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. S ) -op ( if ( R e. LinOp , R , 0hop ) o. T ) ) )
5 1 4 eqeq12d 
 |-  ( R = if ( R e. LinOp , R , 0hop ) -> ( ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) ) <-> ( if ( R e. LinOp , R , 0hop ) o. ( S -op T ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. S ) -op ( if ( R e. LinOp , R , 0hop ) o. T ) ) ) )
6 oveq1 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( S -op T ) = ( if ( S : ~H --> ~H , S , 0hop ) -op T ) )
7 6 coeq2d 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( if ( R e. LinOp , R , 0hop ) o. ( S -op T ) ) = ( if ( R e. LinOp , R , 0hop ) o. ( if ( S : ~H --> ~H , S , 0hop ) -op T ) ) )
8 coeq2 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( if ( R e. LinOp , R , 0hop ) o. S ) = ( if ( R e. LinOp , R , 0hop ) o. if ( S : ~H --> ~H , S , 0hop ) ) )
9 8 oveq1d 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( ( if ( R e. LinOp , R , 0hop ) o. S ) -op ( if ( R e. LinOp , R , 0hop ) o. T ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. if ( S : ~H --> ~H , S , 0hop ) ) -op ( if ( R e. LinOp , R , 0hop ) o. T ) ) )
10 7 9 eqeq12d 
 |-  ( S = if ( S : ~H --> ~H , S , 0hop ) -> ( ( if ( R e. LinOp , R , 0hop ) o. ( S -op T ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. S ) -op ( if ( R e. LinOp , R , 0hop ) o. T ) ) <-> ( if ( R e. LinOp , R , 0hop ) o. ( if ( S : ~H --> ~H , S , 0hop ) -op T ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. if ( S : ~H --> ~H , S , 0hop ) ) -op ( if ( R e. LinOp , R , 0hop ) o. T ) ) ) )
11 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 ) ) )
12 11 coeq2d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( if ( R e. LinOp , R , 0hop ) o. ( if ( S : ~H --> ~H , S , 0hop ) -op T ) ) = ( if ( R e. LinOp , R , 0hop ) o. ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) ) )
13 coeq2 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( if ( R e. LinOp , R , 0hop ) o. T ) = ( if ( R e. LinOp , R , 0hop ) o. if ( T : ~H --> ~H , T , 0hop ) ) )
14 13 oveq2d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( ( if ( R e. LinOp , R , 0hop ) o. if ( S : ~H --> ~H , S , 0hop ) ) -op ( if ( R e. LinOp , R , 0hop ) o. T ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. if ( S : ~H --> ~H , S , 0hop ) ) -op ( if ( R e. LinOp , R , 0hop ) o. if ( T : ~H --> ~H , T , 0hop ) ) ) )
15 12 14 eqeq12d 
 |-  ( T = if ( T : ~H --> ~H , T , 0hop ) -> ( ( if ( R e. LinOp , R , 0hop ) o. ( if ( S : ~H --> ~H , S , 0hop ) -op T ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. if ( S : ~H --> ~H , S , 0hop ) ) -op ( if ( R e. LinOp , R , 0hop ) o. T ) ) <-> ( if ( R e. LinOp , R , 0hop ) o. ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. if ( S : ~H --> ~H , S , 0hop ) ) -op ( if ( R e. LinOp , R , 0hop ) o. if ( T : ~H --> ~H , T , 0hop ) ) ) ) )
16 0lnop 
 |-  0hop e. LinOp
17 16 elimel 
 |-  if ( R e. LinOp , R , 0hop ) e. LinOp
18 ho0f 
 |-  0hop : ~H --> ~H
19 18 elimf 
 |-  if ( S : ~H --> ~H , S , 0hop ) : ~H --> ~H
20 18 elimf 
 |-  if ( T : ~H --> ~H , T , 0hop ) : ~H --> ~H
21 17 19 20 hoddii 
 |-  ( if ( R e. LinOp , R , 0hop ) o. ( if ( S : ~H --> ~H , S , 0hop ) -op if ( T : ~H --> ~H , T , 0hop ) ) ) = ( ( if ( R e. LinOp , R , 0hop ) o. if ( S : ~H --> ~H , S , 0hop ) ) -op ( if ( R e. LinOp , R , 0hop ) o. if ( T : ~H --> ~H , T , 0hop ) ) )
22 5 10 15 21 dedth3h 
 |-  ( ( R e. LinOp /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) ) )