# Metamath Proof Explorer

## Theorem lnopmul

Description: Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopmul ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{\cdot }_{ℎ}{T}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
2 lnopl ${⊢}\left(\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\right)\wedge \left({B}\in ℋ\wedge {0}_{ℎ}\in ℋ\right)\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
3 1 2 mpanr2 ${⊢}\left(\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\right)\wedge {B}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
4 3 3impa ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
5 hvmulcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{ℎ}{B}\in ℋ$
6 ax-hvaddid ${⊢}{A}{\cdot }_{ℎ}{B}\in ℋ\to \left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}={A}{\cdot }_{ℎ}{B}$
7 5 6 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}={A}{\cdot }_{ℎ}{B}$
8 7 3adant1 ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}={A}{\cdot }_{ℎ}{B}$
9 8 fveq2d ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}{0}_{ℎ}\right)={T}\left({A}{\cdot }_{ℎ}{B}\right)$
10 lnop0 ${⊢}{T}\in \mathrm{LinOp}\to {T}\left({0}_{ℎ}\right)={0}_{ℎ}$
11 10 oveq2d ${⊢}{T}\in \mathrm{LinOp}\to \left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{0}_{ℎ}$
12 11 3ad2ant1 ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)=\left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{0}_{ℎ}$
13 lnopf ${⊢}{T}\in \mathrm{LinOp}\to {T}:ℋ⟶ℋ$
14 13 ffvelrnda ${⊢}\left({T}\in \mathrm{LinOp}\wedge {B}\in ℋ\right)\to {T}\left({B}\right)\in ℋ$
15 hvmulcl ${⊢}\left({A}\in ℂ\wedge {T}\left({B}\right)\in ℋ\right)\to {A}{\cdot }_{ℎ}{T}\left({B}\right)\in ℋ$
16 14 15 sylan2 ${⊢}\left({A}\in ℂ\wedge \left({T}\in \mathrm{LinOp}\wedge {B}\in ℋ\right)\right)\to {A}{\cdot }_{ℎ}{T}\left({B}\right)\in ℋ$
17 16 3impb ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{LinOp}\wedge {B}\in ℋ\right)\to {A}{\cdot }_{ℎ}{T}\left({B}\right)\in ℋ$
18 17 3com12 ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{ℎ}{T}\left({B}\right)\in ℋ$
19 ax-hvaddid ${⊢}{A}{\cdot }_{ℎ}{T}\left({B}\right)\in ℋ\to \left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{0}_{ℎ}={A}{\cdot }_{ℎ}{T}\left({B}\right)$
20 18 19 syl ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{0}_{ℎ}={A}{\cdot }_{ℎ}{T}\left({B}\right)$
21 12 20 eqtrd ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{T}\left({B}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)={A}{\cdot }_{ℎ}{T}\left({B}\right)$
22 4 9 21 3eqtr3d ${⊢}\left({T}\in \mathrm{LinOp}\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{B}\right)={A}{\cdot }_{ℎ}{T}\left({B}\right)$