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