Theorem hosd1i

Description: Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hosd1.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
	hosd1.3	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
Assertion	hosd1i	$$⊢T{+}_{\mathrm{op}}U=T{-}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2		hosd1.3	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
3		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
4	3 2	hosubcli	$$⊢\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
5	1 2	hoaddcli	$$⊢\left(T{+}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
6	4 5	hoaddcomi	$$⊢\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)=\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$
7	5 3 2	hoaddsubassi	$$⊢\left(\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}U=\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$
8	6 7	eqtr4i	$$⊢\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)=\left(\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}U$$
9	5	hoaddid1i	$$⊢\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T{+}_{\mathrm{op}}U$$
10	9	oveq1i	$$⊢\left(\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}U=\left(T{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U$$
11	1 2 2	hoaddsubi	$$⊢\left(T{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U=\left(T{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}U$$
12	1 2	hosubcli	$$⊢\left(T{-}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
13	12 2	hoaddcomi	$$⊢\left(T{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}U=U{+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)$$
14	2 1	hodseqi	$$⊢U{+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=T$$
15	11 13 14	3eqtri	$$⊢\left(T{+}_{\mathrm{op}}U\right){-}_{\mathrm{op}}U=T$$
16	8 10 15	3eqtri	$$⊢\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)=T$$
17	1 4 5	hodsi	$$⊢T{-}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)=T{+}_{\mathrm{op}}U\leftrightarrow \left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)=T$$
18	16 17	mpbir	$$⊢T{-}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)=T{+}_{\mathrm{op}}U$$
19	18	eqcomi	$$⊢T{+}_{\mathrm{op}}U=T{-}_{\mathrm{op}}\left(0_{\mathrm{hop}}{-}_{\mathrm{op}}U\right)$$