Theorem hosubneg

Description: Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

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

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		honegsub	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge \left(-1{·}_{\mathrm{op}}U\right):\mathscr{H}⟶\mathscr{H}\right)\to T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right)=T{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)$$
5	3 4	sylan2	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right)=T{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)$$
6		honegneg	$$⊢U:\mathscr{H}⟶\mathscr{H}\to -1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)=U$$
7	6	oveq2d	$$⊢U:\mathscr{H}⟶\mathscr{H}\to T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right)=T{+}_{\mathrm{op}}U$$
8	7	adantl	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to T{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}U\right)\right)=T{+}_{\mathrm{op}}U$$
9	5 8	eqtr3d	$$⊢\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$$