Metamath Proof Explorer

Theorem lnfnli

Description: Basic 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 lnfnli ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ T ∈ LinFn
2 lnfnl ⊢ T ∈ LinFn ∧ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C
3 1 2 mpanl1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C
4 3 3impb ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⁢ T ⁡ B + T ⁡ C