Theorem honegsubdi2

Description: Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	honegsubdi2	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to -1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=U{-}_{\mathrm{op}}T$$

Proof

Step	Hyp	Ref	Expression
1		honegsubdi	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to -1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=\left(-1{·}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U$$
2		neg1cn	$$⊢-1\in ℂ$$
3		homulcl	$$⊢\left(-1\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(-1{·}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
4	2 3	mpan	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(-1{·}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
5		hoaddcom	$$⊢\left(\left(-1{·}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(-1{·}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U=U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)$$
6	4 5	sylan	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(-1{·}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U=U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)$$
7		honegsub	$$⊢\left(U:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=U{-}_{\mathrm{op}}T$$
8	7	ancoms	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to U{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=U{-}_{\mathrm{op}}T$$
9	1 6 8	3eqtrd	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to -1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}U\right)=U{-}_{\mathrm{op}}T$$