This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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