Metamath Proof Explorer

Theorem lnopli

Description: Basic scalar product property of a linear Hilbert space operator. (Contributed by NM, 23-Jan-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnopl.1 ⊢ T ∈ LinOp
Assertion lnopli ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B + ℎ C = A ⋅ ℎ T ⁡ B + ℎ T ⁡ C

Proof

Step Hyp Ref Expression
1 lnopl.1 ⊢ T ∈ LinOp
2 lnopl ⊢ T ∈ LinOp ∧ 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