Metamath Proof Explorer

Theorem lnfnaddmuli

Description: Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 ⊢ T ∈ LinFn
Assertion lnfnaddmuli ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ B + ℎ A ⋅ ℎ C = T ⁡ B + A ⁢ T ⁡ C

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ T ∈ LinFn
2 hvmulcl ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
3 1 lnfnaddi ⊢ B ∈ ℋ ∧ A ⋅ ℎ C ∈ ℋ → T ⁡ B + ℎ A ⋅ ℎ C = T ⁡ B + T ⁡ A ⋅ ℎ C
4 2 3 sylan2 ⊢ B ∈ ℋ ∧ A ∈ ℂ ∧ C ∈ ℋ → T ⁡ B + ℎ A ⋅ ℎ C = T ⁡ B + T ⁡ A ⋅ ℎ C
5 4 3impb ⊢ B ∈ ℋ ∧ A ∈ ℂ ∧ C ∈ ℋ → T ⁡ B + ℎ A ⋅ ℎ C = T ⁡ B + T ⁡ A ⋅ ℎ C
6 5 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ B + ℎ A ⋅ ℎ C = T ⁡ B + T ⁡ A ⋅ ℎ C
7 1 lnfnmuli ⊢ A ∈ ℂ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ C = A ⁢ T ⁡ C
8 7 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ C = A ⁢ T ⁡ C
9 8 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ B + T ⁡ A ⋅ ℎ C = T ⁡ B + A ⁢ T ⁡ C
10 6 9 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ B + ℎ A ⋅ ℎ C = T ⁡ B + A ⁢ T ⁡ C