# Metamath Proof Explorer

## Theorem hosval

Description: Value of the sum of two Hilbert space operators. (Contributed by NM, 10-Nov-2000) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {A}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({A}\right)={S}\left({A}\right){+}_{ℎ}{T}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 hosmval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}{T}=\left({x}\in ℋ⟼{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)$
2 1 fveq1d ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({A}\right)=\left({x}\in ℋ⟼{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)\left({A}\right)$
3 fveq2 ${⊢}{x}={A}\to {S}\left({x}\right)={S}\left({A}\right)$
4 fveq2 ${⊢}{x}={A}\to {T}\left({x}\right)={T}\left({A}\right)$
5 3 4 oveq12d ${⊢}{x}={A}\to {S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)={S}\left({A}\right){+}_{ℎ}{T}\left({A}\right)$
6 eqid ${⊢}\left({x}\in ℋ⟼{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)=\left({x}\in ℋ⟼{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)$
7 ovex ${⊢}{S}\left({A}\right){+}_{ℎ}{T}\left({A}\right)\in \mathrm{V}$
8 5 6 7 fvmpt ${⊢}{A}\in ℋ\to \left({x}\in ℋ⟼{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)\left({A}\right)={S}\left({A}\right){+}_{ℎ}{T}\left({A}\right)$
9 2 8 sylan9eq ${⊢}\left(\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\wedge {A}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({A}\right)={S}\left({A}\right){+}_{ℎ}{T}\left({A}\right)$
10 9 3impa ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {A}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({A}\right)={S}\left({A}\right){+}_{ℎ}{T}\left({A}\right)$