Theorem hosubsub

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

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

Proof

Step	Hyp	Ref	Expression
1		hosubsub2	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to S{-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=S{+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
2		hoaddsubass	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}T=S{+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
3		hoaddsub	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}T=\left(S{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U$$
4	2 3	eqtr3d	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)=\left(S{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U$$
5	4	3com23	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)=\left(S{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U$$
6	1 5	eqtrd	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to S{-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U$$