Theorem honegsub

Description: Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	honegsub	$$⊢\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$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)$$
2		oveq1	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to T{-}_{\mathrm{op}}U=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}U$$
3	1 2	eqeq12d	$$⊢T=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right)\to \left(T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=T{-}_{\mathrm{op}}U\leftrightarrow if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}U\right)$$
4		oveq2	$$⊢U=if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)\to -1{·}_{\mathrm{op}}U=-1{·}_{\mathrm{op}}if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)$$
5	4	oveq2d	$$⊢U=if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)\to if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)\right)$$
6		oveq2	$$⊢U=if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)\to if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}U=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)$$
7	5 6	eqeq12d	$$⊢U=if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)\to \left(if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}U\leftrightarrow if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)\right)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)\right)$$
8		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
9	8	elimf	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
10	8	elimf	$$⊢if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
11	9 10	honegsubi	$$⊢if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)\right)=if\left(T:\mathscr{H}⟶\mathscr{H},T,0_{\mathrm{hop}}\right){-}_{\mathrm{op}}if\left(U:\mathscr{H}⟶\mathscr{H},U,0_{\mathrm{hop}}\right)$$
12	3 7 11	dedth2h	$$⊢\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$$