# Metamath Proof Explorer

## Theorem pjsdi2i

Description: Chained distributive law for Hilbert space operator difference. (Contributed by NM, 30-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjsdi2.1
`|- H e. CH`
pjsdi2.2
`|- R : ~H --> ~H`
pjsdi2.3
`|- S : ~H --> ~H`
pjsdi2.4
`|- T : ~H --> ~H`
Assertion pjsdi2i
`|- ( ( R o. ( S +op T ) ) = ( ( R o. S ) +op ( R o. T ) ) -> ( ( ( projh ` H ) o. R ) o. ( S +op T ) ) = ( ( ( ( projh ` H ) o. R ) o. S ) +op ( ( ( projh ` H ) o. R ) o. T ) ) )`

### Proof

Step Hyp Ref Expression
1 pjsdi2.1
` |-  H e. CH`
2 pjsdi2.2
` |-  R : ~H --> ~H`
3 pjsdi2.3
` |-  S : ~H --> ~H`
4 pjsdi2.4
` |-  T : ~H --> ~H`
5 coeq2
` |-  ( ( R o. ( S +op T ) ) = ( ( R o. S ) +op ( R o. T ) ) -> ( ( projh ` H ) o. ( R o. ( S +op T ) ) ) = ( ( projh ` H ) o. ( ( R o. S ) +op ( R o. T ) ) ) )`
6 2 3 hocofi
` |-  ( R o. S ) : ~H --> ~H`
7 2 4 hocofi
` |-  ( R o. T ) : ~H --> ~H`
8 1 6 7 pjsdii
` |-  ( ( projh ` H ) o. ( ( R o. S ) +op ( R o. T ) ) ) = ( ( ( projh ` H ) o. ( R o. S ) ) +op ( ( projh ` H ) o. ( R o. T ) ) )`
9 5 8 syl6eq
` |-  ( ( R o. ( S +op T ) ) = ( ( R o. S ) +op ( R o. T ) ) -> ( ( projh ` H ) o. ( R o. ( S +op T ) ) ) = ( ( ( projh ` H ) o. ( R o. S ) ) +op ( ( projh ` H ) o. ( R o. T ) ) ) )`
10 coass
` |-  ( ( ( projh ` H ) o. R ) o. ( S +op T ) ) = ( ( projh ` H ) o. ( R o. ( S +op T ) ) )`
11 coass
` |-  ( ( ( projh ` H ) o. R ) o. S ) = ( ( projh ` H ) o. ( R o. S ) )`
12 coass
` |-  ( ( ( projh ` H ) o. R ) o. T ) = ( ( projh ` H ) o. ( R o. T ) )`
13 11 12 oveq12i
` |-  ( ( ( ( projh ` H ) o. R ) o. S ) +op ( ( ( projh ` H ) o. R ) o. T ) ) = ( ( ( projh ` H ) o. ( R o. S ) ) +op ( ( projh ` H ) o. ( R o. T ) ) )`
14 9 10 13 3eqtr4g
` |-  ( ( R o. ( S +op T ) ) = ( ( R o. S ) +op ( R o. T ) ) -> ( ( ( projh ` H ) o. R ) o. ( S +op T ) ) = ( ( ( ( projh ` H ) o. R ) o. S ) +op ( ( ( projh ` H ) o. R ) o. T ) ) )`