Theorem hoaddcom

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

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

Proof

Step	Hyp	Ref	Expression
1		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$$
2		oveq2	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to T{+}_{\mathrm{op}}S=T{+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)$$
3	1 2	eqeq12d	$$⊢S=if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\to \left(S{+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}S\leftrightarrow if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)$$
4		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)$$
5		oveq1	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to T{+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)$$
6	4 5	eqeq12d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\leftrightarrow 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)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)\right)$$
7		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
8	7	elimf	$$⊢if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
9	7	elimf	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
10	8 9	hoaddcomi	$$⊢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)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}if\left(S:\mathscr{H}⟶\mathscr{H},S,0_{\mathrm{hop}}\right)$$
11	3 6 10	dedth2h	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}S$$