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 ∈ LinFn
Assertion lnfnmuli ⊢ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⁢ T ⁡ B

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ T ∈ LinFn
2 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
3 1 lnfnli ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ 0 ℎ ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ 0 ℎ = A ⁢ T ⁡ B + T ⁡ 0 ℎ
4 2 3 mp3an3 ⊢ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ 0 ℎ = A ⁢ T ⁡ B + T ⁡ 0 ℎ
5 hvmulcl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B ∈ ℋ
6 ax-hvaddid ⊢ A ⋅ ℎ B ∈ ℋ → A ⋅ ℎ B + ℎ 0 ℎ = A ⋅ ℎ B
7 5 6 syl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B + ℎ 0 ℎ = A ⋅ ℎ B
8 7 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ 0 ℎ = T ⁡ A ⋅ ℎ B
9 1 lnfn0i ⊢ T ⁡ 0 ℎ = 0
10 9 oveq2i ⊢ A ⁢ T ⁡ B + T ⁡ 0 ℎ = A ⁢ T ⁡ B + 0
11 1 lnfnfi ⊢ T : ℋ ⟶ ℂ
12 11 ffvelrni ⊢ B ∈ ℋ → T ⁡ B ∈ ℂ
13 mulcl ⊢ A ∈ ℂ ∧ T ⁡ B ∈ ℂ → A ⁢ T ⁡ B ∈ ℂ
14 12 13 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⁢ T ⁡ B ∈ ℂ
15 14 addid1d ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⁢ T ⁡ B + 0 = A ⁢ T ⁡ B
16 10 15 syl5eq ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⁢ T ⁡ B + T ⁡ 0 ℎ = A ⁢ T ⁡ B
17 4 8 16 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⁢ T ⁡ B