Theorem hosubadd4

Description: Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hosubcl	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{-}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}$$
2		hosubsub2	$$⊢\left(\left(R{-}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{-}_{\mathrm{op}}S\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=\left(R{-}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
3	2	3expb	$$⊢\left(\left(R{-}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(R{-}_{\mathrm{op}}S\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=\left(R{-}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
4	1 3	sylan	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(R{-}_{\mathrm{op}}S\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=\left(R{-}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
5		hosub4	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(R{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)=\left(R{-}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
6	5	an42s	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(R{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)=\left(R{-}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
7	4 6	eqtr4d	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(R{-}_{\mathrm{op}}S\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=\left(R{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$