# Metamath Proof Explorer

## Theorem lnopmulsubi

Description: Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005) (New usage is discouraged.)

Ref Expression
Hypothesis lnopl.1 ${⊢}{T}\in \mathrm{LinOp}$
Assertion lnopmulsubi ${⊢}\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 hvmulcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{ℎ}{B}\in ℋ$
3 1 lnopsubi ${⊢}\left({A}{\cdot }_{ℎ}{B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){-}_{ℎ}{C}\right)={T}\left({A}{\cdot }_{ℎ}{B}\right){-}_{ℎ}{T}\left({C}\right)$
4 2 3 stoic3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){-}_{ℎ}{C}\right)={T}\left({A}{\cdot }_{ℎ}{B}\right){-}_{ℎ}{T}\left({C}\right)$
5 1 lnopmuli ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{\cdot }_{ℎ}{T}\left({B}\right)$
6 5 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{\cdot }_{ℎ}{T}\left({B}\right)$
7 6 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right){-}_{ℎ}{T}\left({C}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){-}_{ℎ}{T}\left({C}\right)$
8 4 7 eqtrd ${⊢}\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)$