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