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