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 e. LinOp
	lnopco.2	|- T e. LinOp
Assertion	lnophdi	|- ( S -op T ) e. LinOp

Proof

Step	Hyp	Ref	Expression
1		lnopco.1	|- S e. LinOp
2		lnopco.2	|- T e. LinOp
3	1	lnopfi	|- S : ~H --> ~H
4	2	lnopfi	|- T : ~H --> ~H
5	3 4	honegsubi	|- ( S +op ( -u 1 .op T ) ) = ( S -op T )
6		neg1cn	|- -u 1 e. CC
7	2	lnopmi	|- ( -u 1 e. CC -> ( -u 1 .op T ) e. LinOp )
8	6 7	ax-mp	|- ( -u 1 .op T ) e. LinOp
9	1 8	lnophsi	|- ( S +op ( -u 1 .op T ) ) e. LinOp
10	5 9	eqeltrri	|- ( S -op T ) e. LinOp