# Metamath Proof Explorer

Description: Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 lnopl.1 ${⊢}{T}\in \mathrm{LinOp}$
2 ax-1cn ${⊢}1\in ℂ$
3 1 lnopli ${⊢}\left(1\in ℂ\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left(\left(1{\cdot }_{ℎ}{A}\right){+}_{ℎ}{B}\right)=\left(1{\cdot }_{ℎ}{T}\left({A}\right)\right){+}_{ℎ}{T}\left({B}\right)$
4 2 3 mp3an1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left(\left(1{\cdot }_{ℎ}{A}\right){+}_{ℎ}{B}\right)=\left(1{\cdot }_{ℎ}{T}\left({A}\right)\right){+}_{ℎ}{T}\left({B}\right)$
5 ax-hvmulid ${⊢}{A}\in ℋ\to 1{\cdot }_{ℎ}{A}={A}$
6 5 fvoveq1d ${⊢}{A}\in ℋ\to {T}\left(\left(1{\cdot }_{ℎ}{A}\right){+}_{ℎ}{B}\right)={T}\left({A}{+}_{ℎ}{B}\right)$
7 6 adantr ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left(\left(1{\cdot }_{ℎ}{A}\right){+}_{ℎ}{B}\right)={T}\left({A}{+}_{ℎ}{B}\right)$
8 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
9 8 ffvelrni ${⊢}{A}\in ℋ\to {T}\left({A}\right)\in ℋ$
10 ax-hvmulid ${⊢}{T}\left({A}\right)\in ℋ\to 1{\cdot }_{ℎ}{T}\left({A}\right)={T}\left({A}\right)$
11 9 10 syl ${⊢}{A}\in ℋ\to 1{\cdot }_{ℎ}{T}\left({A}\right)={T}\left({A}\right)$
12 11 adantr ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to 1{\cdot }_{ℎ}{T}\left({A}\right)={T}\left({A}\right)$
13 12 oveq1d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left(1{\cdot }_{ℎ}{T}\left({A}\right)\right){+}_{ℎ}{T}\left({B}\right)={T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)$
14 4 7 13 3eqtr3d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{+}_{ℎ}{B}\right)={T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)$