# Metamath Proof Explorer

## Theorem lnfnmul

Description: Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfnmul ${⊢}\left({T}\in \mathrm{LinFn}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{T}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 fveq1 ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({A}{\cdot }_{ℎ}{B}\right)$
2 fveq1 ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to {T}\left({B}\right)=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({B}\right)$
3 2 oveq2d ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to {A}{T}\left({B}\right)={A}if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({B}\right)$
4 1 3 eqeq12d ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to \left({T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{T}\left({B}\right)↔if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({A}{\cdot }_{ℎ}{B}\right)={A}if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({B}\right)\right)$
5 4 imbi2d ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to \left(\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{T}\left({B}\right)\right)↔\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\to if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({A}{\cdot }_{ℎ}{B}\right)={A}if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({B}\right)\right)\right)$
6 0lnfn ${⊢}ℋ×\left\{0\right\}\in \mathrm{LinFn}$
7 6 elimel ${⊢}if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\in \mathrm{LinFn}$
8 7 lnfnmuli ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({A}{\cdot }_{ℎ}{B}\right)={A}if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({B}\right)$
9 5 8 dedth ${⊢}{T}\in \mathrm{LinFn}\to \left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{T}\left({B}\right)\right)$
10 9 3impib ${⊢}\left({T}\in \mathrm{LinFn}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{T}\left({B}\right)$