# Metamath Proof Explorer

## Theorem lnfnsubi

Description: Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 ${⊢}{T}\in \mathrm{LinFn}$
Assertion lnfnsubi ${⊢}\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 lnfnl.1 ${⊢}{T}\in \mathrm{LinFn}$
2 neg1cn ${⊢}-1\in ℂ$
3 1 lnfnaddmuli ${⊢}\left(-1\in ℂ\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right)={T}\left({A}\right)+-1{T}\left({B}\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)+-1{T}\left({B}\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 lnfnfi ${⊢}{T}:ℋ⟶ℂ$
8 7 ffvelrni ${⊢}{A}\in ℋ\to {T}\left({A}\right)\in ℂ$
9 7 ffvelrni ${⊢}{B}\in ℋ\to {T}\left({B}\right)\in ℂ$
10 mulm1 ${⊢}{T}\left({B}\right)\in ℂ\to -1{T}\left({B}\right)=-{T}\left({B}\right)$
11 10 oveq2d ${⊢}{T}\left({B}\right)\in ℂ\to {T}\left({A}\right)+-1{T}\left({B}\right)={T}\left({A}\right)+\left(-{T}\left({B}\right)\right)$
12 11 adantl ${⊢}\left({T}\left({A}\right)\in ℂ\wedge {T}\left({B}\right)\in ℂ\right)\to {T}\left({A}\right)+-1{T}\left({B}\right)={T}\left({A}\right)+\left(-{T}\left({B}\right)\right)$
13 negsub ${⊢}\left({T}\left({A}\right)\in ℂ\wedge {T}\left({B}\right)\in ℂ\right)\to {T}\left({A}\right)+\left(-{T}\left({B}\right)\right)={T}\left({A}\right)-{T}\left({B}\right)$
14 12 13 eqtr2d ${⊢}\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)+-1{T}\left({B}\right)$
15 8 9 14 syl2an ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right)-{T}\left({B}\right)={T}\left({A}\right)+-1{T}\left({B}\right)$
16 4 6 15 3eqtr4d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{-}_{ℎ}{B}\right)={T}\left({A}\right)-{T}\left({B}\right)$