# Metamath Proof Explorer

## Theorem lnopsubi

Description: Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005) (New usage is discouraged.)

Ref Expression
Hypothesis lnopl.1 ${⊢}{T}\in \mathrm{LinOp}$
Assertion lnopsubi ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{-}_{ℎ}{B}\right)={T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 lnopl.1 ${⊢}{T}\in \mathrm{LinOp}$
2 neg1cn ${⊢}-1\in ℂ$
3 1 lnopaddmuli ${⊢}\left(-1\in ℂ\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)={T}\left({A}\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{T}\left({B}\right)\right)$
4 2 3 mp3an1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)={T}\left({A}\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{T}\left({B}\right)\right)$
5 hvsubval ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{-}_{ℎ}{B}={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)$
6 5 fveq2d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{-}_{ℎ}{B}\right)={T}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)$
7 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
8 7 ffvelrni ${⊢}{A}\in ℋ\to {T}\left({A}\right)\in ℋ$
9 7 ffvelrni ${⊢}{B}\in ℋ\to {T}\left({B}\right)\in ℋ$
10 hvsubval ${⊢}\left({T}\left({A}\right)\in ℋ\wedge {T}\left({B}\right)\in ℋ\right)\to {T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)={T}\left({A}\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{T}\left({B}\right)\right)$
11 8 9 10 syl2an ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)={T}\left({A}\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{T}\left({B}\right)\right)$
12 4 6 11 3eqtr4d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{-}_{ℎ}{B}\right)={T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)$