Theorem hoaddassi

Description: Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hods.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
	hods.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hods.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hoaddassi	$$⊢\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		hods.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
2		hods.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
3		hods.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
4		hosval	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}S\right)\left(x\right)=R\left(x\right){+}_{ℎ}S\left(x\right)$$
5	1 2 4	mp3an12	$$⊢x\in \mathscr{H}\to \left(R{+}_{\mathrm{op}}S\right)\left(x\right)=R\left(x\right){+}_{ℎ}S\left(x\right)$$
6	5	oveq1d	$$⊢x\in \mathscr{H}\to \left(R{+}_{\mathrm{op}}S\right)\left(x\right){+}_{ℎ}T\left(x\right)=\left(R\left(x\right){+}_{ℎ}S\left(x\right)\right){+}_{ℎ}T\left(x\right)$$
7	1 2	hoaddcli	$$⊢\left(R{+}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}$$
8		hosval	$$⊢\left(\left(R{+}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right)\left(x\right)=\left(R{+}_{\mathrm{op}}S\right)\left(x\right){+}_{ℎ}T\left(x\right)$$
9	7 3 8	mp3an12	$$⊢x\in \mathscr{H}\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right)\left(x\right)=\left(R{+}_{\mathrm{op}}S\right)\left(x\right){+}_{ℎ}T\left(x\right)$$
10		hosval	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right)\left(x\right)=S\left(x\right){+}_{ℎ}T\left(x\right)$$
11	2 3 10	mp3an12	$$⊢x\in \mathscr{H}\to \left(S{+}_{\mathrm{op}}T\right)\left(x\right)=S\left(x\right){+}_{ℎ}T\left(x\right)$$
12	11	oveq2d	$$⊢x\in \mathscr{H}\to R\left(x\right){+}_{ℎ}\left(S{+}_{\mathrm{op}}T\right)\left(x\right)=R\left(x\right){+}_{ℎ}\left(S\left(x\right){+}_{ℎ}T\left(x\right)\right)$$
13	2 3	hoaddcli	$$⊢\left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
14		hosval	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge \left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\right)\left(x\right)=R\left(x\right){+}_{ℎ}\left(S{+}_{\mathrm{op}}T\right)\left(x\right)$$
15	1 13 14	mp3an12	$$⊢x\in \mathscr{H}\to \left(R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\right)\left(x\right)=R\left(x\right){+}_{ℎ}\left(S{+}_{\mathrm{op}}T\right)\left(x\right)$$
16	1	ffvelcdmi	$$⊢x\in \mathscr{H}\to R\left(x\right)\in \mathscr{H}$$
17	2	ffvelcdmi	$$⊢x\in \mathscr{H}\to S\left(x\right)\in \mathscr{H}$$
18	3	ffvelcdmi	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
19		ax-hvass	$$⊢\left(R\left(x\right)\in \mathscr{H}\wedge S\left(x\right)\in \mathscr{H}\wedge T\left(x\right)\in \mathscr{H}\right)\to \left(R\left(x\right){+}_{ℎ}S\left(x\right)\right){+}_{ℎ}T\left(x\right)=R\left(x\right){+}_{ℎ}\left(S\left(x\right){+}_{ℎ}T\left(x\right)\right)$$
20	16 17 18 19	syl3anc	$$⊢x\in \mathscr{H}\to \left(R\left(x\right){+}_{ℎ}S\left(x\right)\right){+}_{ℎ}T\left(x\right)=R\left(x\right){+}_{ℎ}\left(S\left(x\right){+}_{ℎ}T\left(x\right)\right)$$
21	12 15 20	3eqtr4d	$$⊢x\in \mathscr{H}\to \left(R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\right)\left(x\right)=\left(R\left(x\right){+}_{ℎ}S\left(x\right)\right){+}_{ℎ}T\left(x\right)$$
22	6 9 21	3eqtr4d	$$⊢x\in \mathscr{H}\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right)\left(x\right)=\left(R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\right)\left(x\right)$$
23	22	rgen	$$⊢\forall x\in \mathscr{H}\left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right)\left(x\right)=\left(R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\right)\left(x\right)$$
24	7 3	hoaddcli	$$⊢\left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
25	1 13	hoaddcli	$$⊢\left(R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\right):\mathscr{H}⟶\mathscr{H}$$
26	24 25	hoeqi	$$⊢\forall x\in \mathscr{H}\left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right)\left(x\right)=\left(R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\right)\left(x\right)\leftrightarrow \left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$
27	23 26	mpbi	$$⊢\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$