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 𝐻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 syl6eq ( ( 𝑅 ∘ ( 𝑆 +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𝐻 ) ∘ 𝑅 ) ∘ 𝑇 ) ) )