# 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 𝑇 ∈ LinFn
Assertion lnfnmuli ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑇𝐵 ) ) )

### Proof

Step Hyp Ref Expression
1 lnfnl.1 𝑇 ∈ LinFn
2 ax-hv0cl 0 ∈ ℋ
3 1 lnfnli ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 0 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝐴 · 𝐵 ) + 0 ) ) = ( ( 𝐴 · ( 𝑇𝐵 ) ) + ( 𝑇 ‘ 0 ) ) )
4 2 3 mp3an3 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝐴 · 𝐵 ) + 0 ) ) = ( ( 𝐴 · ( 𝑇𝐵 ) ) + ( 𝑇 ‘ 0 ) ) )
5 hvmulcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 · 𝐵 ) ∈ ℋ )
6 ax-hvaddid ( ( 𝐴 · 𝐵 ) ∈ ℋ → ( ( 𝐴 · 𝐵 ) + 0 ) = ( 𝐴 · 𝐵 ) )
7 5 6 syl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 · 𝐵 ) + 0 ) = ( 𝐴 · 𝐵 ) )
8 7 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝐴 · 𝐵 ) + 0 ) ) = ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) )
9 1 lnfn0i ( 𝑇 ‘ 0 ) = 0
10 9 oveq2i ( ( 𝐴 · ( 𝑇𝐵 ) ) + ( 𝑇 ‘ 0 ) ) = ( ( 𝐴 · ( 𝑇𝐵 ) ) + 0 )
11 1 lnfnfi 𝑇 : ℋ ⟶ ℂ
12 11 ffvelrni ( 𝐵 ∈ ℋ → ( 𝑇𝐵 ) ∈ ℂ )
13 mulcl ( ( 𝐴 ∈ ℂ ∧ ( 𝑇𝐵 ) ∈ ℂ ) → ( 𝐴 · ( 𝑇𝐵 ) ) ∈ ℂ )
14 12 13 sylan2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 · ( 𝑇𝐵 ) ) ∈ ℂ )
15 14 addid1d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 · ( 𝑇𝐵 ) ) + 0 ) = ( 𝐴 · ( 𝑇𝐵 ) ) )
16 10 15 syl5eq ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 · ( 𝑇𝐵 ) ) + ( 𝑇 ‘ 0 ) ) = ( 𝐴 · ( 𝑇𝐵 ) ) )
17 4 8 16 3eqtr3d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑇𝐵 ) ) )