This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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