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 ⊢ S ∈ LinOp
lnopco.2 ⊢ T ∈ LinOp
Assertion lnophdi ⊢ S - op T ∈ LinOp

Proof

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