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	⊢ 𝑆 ∈ LinOp
	lnopco.2	⊢ 𝑇 ∈ LinOp
Assertion	lnophdi	⊢ ( 𝑆 −op 𝑇 ) ∈ LinOp

Proof

Step	Hyp	Ref	Expression
1		lnopco.1	⊢ 𝑆 ∈ LinOp
2		lnopco.2	⊢ 𝑇 ∈ LinOp
3	1	lnopfi	⊢ 𝑆 : ℋ ⟶ ℋ
4	2	lnopfi	⊢ 𝑇 : ℋ ⟶ ℋ
5	3 4	honegsubi	⊢ ( 𝑆 +op ( - 1 ·op 𝑇 ) ) = ( 𝑆 −op 𝑇 )
6		neg1cn	⊢ - 1 ∈ ℂ
7	2	lnopmi	⊢ ( - 1 ∈ ℂ → ( - 1 ·op 𝑇 ) ∈ LinOp )
8	6 7	ax-mp	⊢ ( - 1 ·op 𝑇 ) ∈ LinOp
9	1 8	lnophsi	⊢ ( 𝑆 +op ( - 1 ·op 𝑇 ) ) ∈ LinOp
10	5 9	eqeltrri	⊢ ( 𝑆 −op 𝑇 ) ∈ LinOp