Theorem hosubsub2

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

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		hosubcl	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(T{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
2		honegsub	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge \left(T{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)\right)=S{-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)$$
3	1 2	sylan2	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)\right)=S{-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)$$
4	3	3impb	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)\right)=S{-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)$$
5		honegsubdi2	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to -1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=U{-}_{\mathrm{op}}T$$
6	5	oveq2d	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)\right)=S{+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
7	6	3adant1	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)\right)=S{+}_{\mathrm{op}}\left(U{-}_{\mathrm{op}}T\right)$$
8	4 7	eqtr3d	$$⊢\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)$$