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	⊢ 𝐻 ∈ Cℋ
	pjsdi2.2	⊢ 𝑅 : ℋ ⟶ ℋ
	pjsdi2.3	⊢ 𝑆 : ℋ ⟶ ℋ
	pjsdi2.4	⊢ 𝑇 : ℋ ⟶ ℋ
Assertion	pjsdi2i	⊢ ( ( 𝑅 ∘ ( 𝑆 +op 𝑇 ) ) = ( ( 𝑅 ∘ 𝑆 ) +op ( 𝑅 ∘ 𝑇 ) ) → ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ ( 𝑆 +op 𝑇 ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ 𝑆 ) +op ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjsdi2.1	⊢ 𝐻 ∈ Cℋ
2		pjsdi2.2	⊢ 𝑅 : ℋ ⟶ ℋ
3		pjsdi2.3	⊢ 𝑆 : ℋ ⟶ ℋ
4		pjsdi2.4	⊢ 𝑇 : ℋ ⟶ ℋ
5		coeq2	⊢ ( ( 𝑅 ∘ ( 𝑆 +op 𝑇 ) ) = ( ( 𝑅 ∘ 𝑆 ) +op ( 𝑅 ∘ 𝑇 ) ) → ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ ( 𝑆 +op 𝑇 ) ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( ( 𝑅 ∘ 𝑆 ) +op ( 𝑅 ∘ 𝑇 ) ) ) )
6	2 3	hocofi	⊢ ( 𝑅 ∘ 𝑆 ) : ℋ ⟶ ℋ
7	2 4	hocofi	⊢ ( 𝑅 ∘ 𝑇 ) : ℋ ⟶ ℋ
8	1 6 7	pjsdii	⊢ ( ( projℎ ‘ 𝐻 ) ∘ ( ( 𝑅 ∘ 𝑆 ) +op ( 𝑅 ∘ 𝑇 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ 𝑆 ) ) +op ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ 𝑇 ) ) )
9	5 8	eqtrdi	⊢ ( ( 𝑅 ∘ ( 𝑆 +op 𝑇 ) ) = ( ( 𝑅 ∘ 𝑆 ) +op ( 𝑅 ∘ 𝑇 ) ) → ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ ( 𝑆 +op 𝑇 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ 𝑆 ) ) +op ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ 𝑇 ) ) ) )
10		coass	⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ ( 𝑆 +op 𝑇 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ ( 𝑆 +op 𝑇 ) ) )
11		coass	⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ 𝑆 ) = ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ 𝑆 ) )
12		coass	⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ 𝑇 ) = ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ 𝑇 ) )
13	11 12	oveq12i	⊢ ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ 𝑆 ) +op ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ 𝑇 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ 𝑆 ) ) +op ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑅 ∘ 𝑇 ) ) )
14	9 10 13	3eqtr4g	⊢ ( ( 𝑅 ∘ ( 𝑆 +op 𝑇 ) ) = ( ( 𝑅 ∘ 𝑆 ) +op ( 𝑅 ∘ 𝑇 ) ) → ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ ( 𝑆 +op 𝑇 ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ 𝑆 ) +op ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑅 ) ∘ 𝑇 ) ) )