# Metamath Proof Explorer

## Definition df-hodif

Description: Define the difference of two Hilbert space operators. Definition of Beran p. 111. (Contributed by NM, 9-Nov-2000) (New usage is discouraged.)

Ref Expression
Assertion df-hodif ${⊢}{-}_{\mathrm{op}}=\left({f}\in \left({ℋ}^{ℋ}\right),{g}\in \left({ℋ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}\left({x}\right){-}_{ℎ}{g}\left({x}\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chod ${class}{-}_{\mathrm{op}}$
1 vf ${setvar}{f}$
2 chba ${class}ℋ$
3 cmap ${class}{↑}_{𝑚}$
4 2 2 3 co ${class}\left({ℋ}^{ℋ}\right)$
5 vg ${setvar}{g}$
6 vx ${setvar}{x}$
7 1 cv ${setvar}{f}$
8 6 cv ${setvar}{x}$
9 8 7 cfv ${class}{f}\left({x}\right)$
10 cmv ${class}{-}_{ℎ}$
11 5 cv ${setvar}{g}$
12 8 11 cfv ${class}{g}\left({x}\right)$
13 9 12 10 co ${class}\left({f}\left({x}\right){-}_{ℎ}{g}\left({x}\right)\right)$
14 6 2 13 cmpt ${class}\left({x}\in ℋ⟼{f}\left({x}\right){-}_{ℎ}{g}\left({x}\right)\right)$
15 1 5 4 4 14 cmpo ${class}\left({f}\in \left({ℋ}^{ℋ}\right),{g}\in \left({ℋ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}\left({x}\right){-}_{ℎ}{g}\left({x}\right)\right)\right)$
16 0 15 wceq ${wff}{-}_{\mathrm{op}}=\left({f}\in \left({ℋ}^{ℋ}\right),{g}\in \left({ℋ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}\left({x}\right){-}_{ℎ}{g}\left({x}\right)\right)\right)$