Theorem honegdi

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

	Ref	Expression
Assertion	honegdi	$$⊢\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}}\left(-1{·}_{\mathrm{op}}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		neg1cn	$$⊢-1\in ℂ$$
2		hoadddi	$$⊢\left(-1\in ℂ\wedge 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}}\left(-1{·}_{\mathrm{op}}U\right)$$
3	1 2	mp3an1	$$⊢\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}}\left(-1{·}_{\mathrm{op}}U\right)$$