Theorem hosubeq0i

Description: If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hosd1.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
	hosd1.3	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
Assertion	hosubeq0i	$$⊢T{-}_{\mathrm{op}}U=0_{\mathrm{hop}}\leftrightarrow T=U$$

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2		hosd1.3	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
3	1 2	honegsubi	$$⊢T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=T{-}_{\mathrm{op}}U$$
4	3	eqeq1i	$$⊢T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=0_{\mathrm{hop}}\leftrightarrow T{-}_{\mathrm{op}}U=0_{\mathrm{hop}}$$
5		oveq1	$$⊢T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=0_{\mathrm{hop}}\to \left(T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right){+}_{\mathrm{op}}U=0_{\mathrm{hop}}{+}_{\mathrm{op}}U$$
6	4 5	sylbir	$$⊢T{-}_{\mathrm{op}}U=0_{\mathrm{hop}}\to \left(T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right){+}_{\mathrm{op}}U=0_{\mathrm{hop}}{+}_{\mathrm{op}}U$$
7		neg1cn	$$⊢-1\in ℂ$$
8		homulcl	$$⊢\left(-1\in ℂ\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(-1{·}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
9	7 2 8	mp2an	$$⊢\left(-1{·}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}$$
10	1 9 2	hoadd32i	$$⊢\left(T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right){+}_{\mathrm{op}}U=\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)$$
11	1 2 9	hoaddassi	$$⊢\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=T{+}_{\mathrm{op}}\left(U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right)$$
12	2 2	honegsubi	$$⊢U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=U{-}_{\mathrm{op}}U$$
13	2	hodidi	$$⊢U{-}_{\mathrm{op}}U=0_{\mathrm{hop}}$$
14	12 13	eqtri	$$⊢U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=0_{\mathrm{hop}}$$
15	14	oveq2i	$$⊢T{+}_{\mathrm{op}}\left(U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right)=T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}$$
16	1	hoaddid1i	$$⊢T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$
17	15 16	eqtri	$$⊢T{+}_{\mathrm{op}}\left(U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right)=T$$
18	11 17	eqtri	$$⊢\left(T{+}_{\mathrm{op}}U\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=T$$
19	10 18	eqtri	$$⊢\left(T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right){+}_{\mathrm{op}}U=T$$
20		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
21	20 2	hoaddcomi	$$⊢0_{\mathrm{hop}}{+}_{\mathrm{op}}U=U{+}_{\mathrm{op}}{0}_{\mathrm{hop}}$$
22	2	hoaddid1i	$$⊢U{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=U$$
23	21 22	eqtri	$$⊢0_{\mathrm{hop}}{+}_{\mathrm{op}}U=U$$
24	6 19 23	3eqtr3g	$$⊢T{-}_{\mathrm{op}}U=0_{\mathrm{hop}}\to T=U$$
25		oveq1	$$⊢T=U\to T{-}_{\mathrm{op}}U=U{-}_{\mathrm{op}}U$$
26	25 13	eqtrdi	$$⊢T=U\to T{-}_{\mathrm{op}}U=0_{\mathrm{hop}}$$
27	24 26	impbii	$$⊢T{-}_{\mathrm{op}}U=0_{\mathrm{hop}}\leftrightarrow T=U$$