Theorem hoaddsubass

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

	Ref	Expression
Assertion	hoaddsubass	$$⊢\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		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
2		hosubcl	$$⊢\left(0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
3	1 2	mpan	$$⊢U:\mathscr{H}⟶\mathscr{H}\to \left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
4		hoaddass	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge \left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)=S{+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)\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 \left(S{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)=S{+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)\right)$$
6		hoaddcl	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
7		ho0sub	$$⊢\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}}U=\left(S{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$
8	6 7	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}}U=\left(S{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$
9		ho0sub	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to T{-}_{\mathrm{op}}U=T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$
10	9	3adant1	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to T{-}_{\mathrm{op}}U=T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$
11	10	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}}U\right)=S{+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)\right)$$
12	5 8 11	3eqtr4d	$$⊢\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)$$