# 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}\in \mathrm{LinOp}$
Assertion lnopli ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({C}\right)$

### Proof

Step Hyp Ref Expression
1 lnopl.1 ${⊢}{T}\in \mathrm{LinOp}$
2 lnopl ${⊢}\left(\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\right)\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({C}\right)$
3 1 2 mpanl1 ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({C}\right)$
4 3 3impb ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{C}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({C}\right)$