Theorem hoaddass

Description: Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoaddass	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to R{+}_{\mathrm{op}}S=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}S$$
2	1	oveq1d	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to \left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T$$
3		oveq1	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$
4	2 3	eqeq12d	$$⊢R=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right)\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\leftrightarrow \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\right)$$
5		oveq2	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}S=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)$$
6	5	oveq1d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}T$$
7		oveq1	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to S{+}_{\mathrm{op}}T=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}T$$
8	7	oveq2d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}T\right)$$
9	6 8	eqeq12d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to \left(\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\leftrightarrow \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}T=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}T\right)\right)$$
10		oveq2	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}T=\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
11		oveq2	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}T=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)$$
12	11	oveq2d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}T\right)=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)$$
13	10 12	eqeq12d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}T=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}T\right)\leftrightarrow \left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)\right)$$
14		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
15	14	elimf	$$⊢if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
16	14	elimf	$$⊢if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
17	14	elimf	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
18	15 16 17	hoaddassi	$$⊢\left(if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right){+}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)=if\left(R:\mathscr{H}⟶\mathscr{H},R,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\right)$$
19	4 9 13 18	dedth3h	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$