# Metamath Proof Explorer

## Theorem hosubcli

Description: Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses hoeq.1 ${⊢}{S}:ℋ⟶ℋ$
hoeq.2 ${⊢}{T}:ℋ⟶ℋ$
Assertion hosubcli ${⊢}\left({S}{-}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$

### Proof

Step Hyp Ref Expression
1 hoeq.1 ${⊢}{S}:ℋ⟶ℋ$
2 hoeq.2 ${⊢}{T}:ℋ⟶ℋ$
3 hodmval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to {S}{-}_{\mathrm{op}}{T}=\left({x}\in ℋ⟼{S}\left({x}\right){-}_{ℎ}{T}\left({x}\right)\right)$
4 1 2 3 mp2an ${⊢}{S}{-}_{\mathrm{op}}{T}=\left({x}\in ℋ⟼{S}\left({x}\right){-}_{ℎ}{T}\left({x}\right)\right)$
5 1 ffvelrni ${⊢}{x}\in ℋ\to {S}\left({x}\right)\in ℋ$
6 2 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
7 hvsubcl ${⊢}\left({S}\left({x}\right)\in ℋ\wedge {T}\left({x}\right)\in ℋ\right)\to {S}\left({x}\right){-}_{ℎ}{T}\left({x}\right)\in ℋ$
8 5 6 7 syl2anc ${⊢}{x}\in ℋ\to {S}\left({x}\right){-}_{ℎ}{T}\left({x}\right)\in ℋ$
9 4 8 fmpti ${⊢}\left({S}{-}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$