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 C
pjsdi2.2 R :
pjsdi2.3 S :
pjsdi2.4 T :
Assertion pjsdi2i R S + op T = R S + op R T proj H R S + op T = proj H R S + op proj H R T

Proof

Step Hyp Ref Expression
1 pjsdi2.1 H C
2 pjsdi2.2 R :
3 pjsdi2.3 S :
4 pjsdi2.4 T :
5 coeq2 R S + op T = R S + op R T proj H R S + op T = proj H R S + op R T
6 2 3 hocofi R S :
7 2 4 hocofi R T :
8 1 6 7 pjsdii proj H R S + op R T = proj H R S + op proj H R T
9 5 8 syl6eq R S + op T = R S + op R T proj H R S + op T = proj H R S + op proj H R T
10 coass proj H R S + op T = proj H R S + op T
11 coass proj H R S = proj H R S
12 coass proj H R T = proj H R T
13 11 12 oveq12i proj H R S + op proj H R T = proj H R S + op proj H R T
14 9 10 13 3eqtr4g R S + op T = R S + op R T proj H R S + op T = proj H R S + op proj H R T