Theorem lnophdi

Description: The difference of two linear operators is linear. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnopco.1	$$⊢S\in \mathrm{LinOp}$$
	lnopco.2	$$⊢T\in \mathrm{LinOp}$$
Assertion	lnophdi	$$⊢S{-}_{\mathrm{op}}T\in \mathrm{LinOp}$$

Proof

Step	Hyp	Ref	Expression
1		lnopco.1	$$⊢S\in \mathrm{LinOp}$$
2		lnopco.2	$$⊢T\in \mathrm{LinOp}$$
3	1	lnopfi	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
4	2	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
5	3 4	honegsubi	$$⊢S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=S{-}_{\mathrm{op}}T$$
6		neg1cn	$$⊢-1\in ℂ$$
7	2	lnopmi	$$⊢-1\in ℂ\to -1{·}_{\mathrm{op}}T\in \mathrm{LinOp}$$
8	6 7	ax-mp	$$⊢-1{·}_{\mathrm{op}}T\in \mathrm{LinOp}$$
9	1 8	lnophsi	$$⊢S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\in \mathrm{LinOp}$$
10	5 9	eqeltrri	$$⊢S{-}_{\mathrm{op}}T\in \mathrm{LinOp}$$