Theorem hosubsub4

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

	Ref	Expression
Assertion	hosubsub4	$$⊢\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=S{-}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		neg1cn	$$⊢-1\in ℂ$$
2		homulcl	$$⊢\left(-1\in ℂ\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(-1{·}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
3	1 2	mpan	$$⊢U:\mathscr{H}⟶\mathscr{H}\to \left(-1{·}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
4		hosubsub	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge \left(-1{·}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}\right)\to S{-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right)=\left(S{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)$$
5	3 4	syl3an3	$$⊢\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}}\left(-1{·}_{\mathrm{op}}U\right)\right)=\left(S{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)$$
6		hosubneg	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to T{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=T{+}_{\mathrm{op}}U$$
7	6	3adant1	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to T{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=T{+}_{\mathrm{op}}U$$
8	7	oveq2d	$$⊢\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}}\left(-1{·}_{\mathrm{op}}U\right)\right)=S{-}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)$$
9		hosubcl	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
10		honegsub	$$⊢\left(\left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}T\right){-}_{\mathrm{op}}U$$
11	9 10	stoic3	$$⊢\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}}\left(-1{·}_{\mathrm{op}}U\right)=\left(S{-}_{\mathrm{op}}T\right){-}_{\mathrm{op}}U$$
12	5 8 11	3eqtr3rd	$$⊢\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=S{-}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)$$