Theorem hoaddsub

Description: Law for operator addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hoaddcom	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}S$$
2	1	oveq1d	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right){-}_{\mathrm{op}}U=\left(T{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}U$$
3	2	3adant3	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right){-}_{\mathrm{op}}U=\left(T{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}U$$
4		hoaddsubass	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(T{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}U=T{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}U\right)$$
5	4	3com12	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(T{+}_{\mathrm{op}}S\right){-}_{\mathrm{op}}U=T{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}U\right)$$
6		hosubcl	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
7		hoaddcom	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge \left(S{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}\right)\to T{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}T$$
8	7	ex	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(\left(S{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}\to T{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}T\right)$$
9	6 8	syl5	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to T{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}T\right)$$
10	9	expd	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(S:\mathscr{H}⟶\mathscr{H}\to \left(U:\mathscr{H}⟶\mathscr{H}\to T{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}T\right)\right)$$
11	10	com12	$$⊢S:\mathscr{H}⟶\mathscr{H}\to \left(T:\mathscr{H}⟶\mathscr{H}\to \left(U:\mathscr{H}⟶\mathscr{H}\to T{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}T\right)\right)$$
12	11	3imp	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to T{+}_{\mathrm{op}}\left(S{-}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}T$$
13	3 5 12	3eqtrd	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right){-}_{\mathrm{op}}U=\left(S{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}T$$