Theorem hoaddcomi

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

	Ref	Expression
Hypotheses	hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hoaddcomi	$$⊢S{+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}S$$

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
2		hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
3	1	ffvelrni	$$⊢x\in \mathscr{H}\to S\left(x\right)\in \mathscr{H}$$
4	2	ffvelrni	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
5		ax-hvcom	$$⊢\left(S\left(x\right)\in \mathscr{H}\wedge T\left(x\right)\in \mathscr{H}\right)\to S\left(x\right){+}_{ℎ}T\left(x\right)=T\left(x\right){+}_{ℎ}S\left(x\right)$$
6	3 4 5	syl2anc	$$⊢x\in \mathscr{H}\to S\left(x\right){+}_{ℎ}T\left(x\right)=T\left(x\right){+}_{ℎ}S\left(x\right)$$
7		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)$$
8	1 2 7	mp3an12	$$⊢x\in \mathscr{H}\to \left(S{+}_{\mathrm{op}}T\right)\left(x\right)=S\left(x\right){+}_{ℎ}T\left(x\right)$$
9		hosval	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(T{+}_{\mathrm{op}}S\right)\left(x\right)=T\left(x\right){+}_{ℎ}S\left(x\right)$$
10	2 1 9	mp3an12	$$⊢x\in \mathscr{H}\to \left(T{+}_{\mathrm{op}}S\right)\left(x\right)=T\left(x\right){+}_{ℎ}S\left(x\right)$$
11	6 8 10	3eqtr4d	$$⊢x\in \mathscr{H}\to \left(S{+}_{\mathrm{op}}T\right)\left(x\right)=\left(T{+}_{\mathrm{op}}S\right)\left(x\right)$$
12	11	rgen	$$⊢\forall x\in \mathscr{H}\left(S{+}_{\mathrm{op}}T\right)\left(x\right)=\left(T{+}_{\mathrm{op}}S\right)\left(x\right)$$
13	1 2	hoaddcli	$$⊢\left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
14	2 1	hoaddcli	$$⊢\left(T{+}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}$$
15	13 14	hoeqi	$$⊢\forall x\in \mathscr{H}\left(S{+}_{\mathrm{op}}T\right)\left(x\right)=\left(T{+}_{\mathrm{op}}S\right)\left(x\right)\leftrightarrow S{+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}S$$
16	12 15	mpbi	$$⊢S{+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}S$$