Metamath Proof Explorer

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

Ref Expression
Hypothesis lnopl.1 ${⊢}{T}\in \mathrm{LinOp}$
Assertion lnopaddmuli ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({B}{+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)\right)={T}\left({B}\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({C}\right)\right)$

Proof

Step Hyp Ref Expression
1 lnopl.1 ${⊢}{T}\in \mathrm{LinOp}$
2 hvmulcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{ℎ}{C}\in ℋ$
3 1 lnopaddi ${⊢}\left({B}\in ℋ\wedge {A}{\cdot }_{ℎ}{C}\in ℋ\right)\to {T}\left({B}{+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)\right)={T}\left({B}\right){+}_{ℎ}{T}\left({A}{\cdot }_{ℎ}{C}\right)$
4 2 3 sylan2 ${⊢}\left({B}\in ℋ\wedge \left({A}\in ℂ\wedge {C}\in ℋ\right)\right)\to {T}\left({B}{+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)\right)={T}\left({B}\right){+}_{ℎ}{T}\left({A}{\cdot }_{ℎ}{C}\right)$
5 4 3impb ${⊢}\left({B}\in ℋ\wedge {A}\in ℂ\wedge {C}\in ℋ\right)\to {T}\left({B}{+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)\right)={T}\left({B}\right){+}_{ℎ}{T}\left({A}{\cdot }_{ℎ}{C}\right)$
6 5 3com12 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({B}{+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)\right)={T}\left({B}\right){+}_{ℎ}{T}\left({A}{\cdot }_{ℎ}{C}\right)$
7 1 lnopmuli ${⊢}\left({A}\in ℂ\wedge {C}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{C}\right)={A}{\cdot }_{ℎ}{T}\left({C}\right)$
8 7 3adant2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({A}{\cdot }_{ℎ}{C}\right)={A}{\cdot }_{ℎ}{T}\left({C}\right)$
9 8 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({B}\right){+}_{ℎ}{T}\left({A}{\cdot }_{ℎ}{C}\right)={T}\left({B}\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({C}\right)\right)$
10 6 9 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({B}{+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)\right)={T}\left({B}\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({C}\right)\right)$