# Metamath Proof Explorer

Description: The sum of Hilbert space operators is an operator. (Contributed by NM, 21-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion hoaddcl ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$

### Proof

Step Hyp Ref Expression
1 ffvelrn ${⊢}\left({S}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {S}\left({x}\right)\in ℋ$
2 1 adantlr ${⊢}\left(\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {S}\left({x}\right)\in ℋ$
3 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
4 3 adantll ${⊢}\left(\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
5 hvaddcl ${⊢}\left({S}\left({x}\right)\in ℋ\wedge {T}\left({x}\right)\in ℋ\right)\to {S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\in ℋ$
6 2 4 5 syl2anc ${⊢}\left(\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\in ℋ$
7 6 fmpttd ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({x}\in ℋ⟼{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right):ℋ⟶ℋ$
8 hosmval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}{T}=\left({x}\in ℋ⟼{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)$
9 8 feq1d ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ↔\left({x}\in ℋ⟼{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right):ℋ⟶ℋ\right)$
10 7 9 mpbird ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$