# Metamath Proof Explorer

## Theorem lnfnli

Description: Basic property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 ${⊢}{T}\in \mathrm{LinFn}$
Assertion lnfnli ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)$

### Proof

Step Hyp Ref Expression
1 lnfnl.1 ${⊢}{T}\in \mathrm{LinFn}$
2 lnfnl ${⊢}\left(\left({T}\in \mathrm{LinFn}\wedge {A}\in ℂ\right)\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)$
3 1 2 mpanl1 ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)$
4 3 3impb ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)={A}{T}\left({B}\right)+{T}\left({C}\right)$