# Metamath Proof Explorer

## Theorem lnfnmuli

Description: Multiplicative 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 lnfnmuli ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{T}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 lnfnl.1 ${⊢}{T}\in \mathrm{LinFn}$
2 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
3 1 lnfnli ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {0}_{ℎ}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}\right)={A}{T}\left({B}\right)+{T}\left({0}_{ℎ}\right)$
4 2 3 mp3an3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}\right)={A}{T}\left({B}\right)+{T}\left({0}_{ℎ}\right)$
5 hvmulcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{ℎ}{B}\in ℋ$
6 ax-hvaddid ${⊢}{A}{\cdot }_{ℎ}{B}\in ℋ\to \left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}={A}{\cdot }_{ℎ}{B}$
7 5 6 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}={A}{\cdot }_{ℎ}{B}$
8 7 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}\right)={T}\left({A}{\cdot }_{ℎ}{B}\right)$
9 1 lnfn0i ${⊢}{T}\left({0}_{ℎ}\right)=0$
10 9 oveq2i ${⊢}{A}{T}\left({B}\right)+{T}\left({0}_{ℎ}\right)={A}{T}\left({B}\right)+0$
11 1 lnfnfi ${⊢}{T}:ℋ⟶ℂ$
12 11 ffvelrni ${⊢}{B}\in ℋ\to {T}\left({B}\right)\in ℂ$
13 mulcl ${⊢}\left({A}\in ℂ\wedge {T}\left({B}\right)\in ℂ\right)\to {A}{T}\left({B}\right)\in ℂ$
14 12 13 sylan2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{T}\left({B}\right)\in ℂ$
15 14 addid1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{T}\left({B}\right)+0={A}{T}\left({B}\right)$
16 10 15 syl5eq ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{T}\left({B}\right)+{T}\left({0}_{ℎ}\right)={A}{T}\left({B}\right)$
17 4 8 16 3eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{T}\left({B}\right)$