# Metamath Proof Explorer

## Definition df-hfsum

Description: Define the sum of two Hilbert space functionals. Definition of Beran p. 111. Note that unlike some authors, we define a functional as any function from ~H to CC , not just linear (or bounded linear) ones. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion df-hfsum ${⊢}{+}_{\mathrm{fn}}=\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 chfs ${class}{+}_{\mathrm{fn}}$
1 vf ${setvar}{f}$
2 cc ${class}ℂ$
3 cmap ${class}{↑}_{𝑚}$
4 chba ${class}ℋ$
5 2 4 3 co ${class}\left({ℂ}^{ℋ}\right)$
6 vg ${setvar}{g}$
7 vx ${setvar}{x}$
8 1 cv ${setvar}{f}$
9 7 cv ${setvar}{x}$
10 9 8 cfv ${class}{f}\left({x}\right)$
11 caddc ${class}+$
12 6 cv ${setvar}{g}$
13 9 12 cfv ${class}{g}\left({x}\right)$
14 10 13 11 co ${class}\left({f}\left({x}\right)+{g}\left({x}\right)\right)$
15 7 4 14 cmpt ${class}\left({x}\in ℋ⟼{f}\left({x}\right)+{g}\left({x}\right)\right)$
16 1 6 5 5 15 cmpo ${class}\left({f}\in \left({ℂ}^{ℋ}\right),{g}\in \left({ℂ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}\left({x}\right)+{g}\left({x}\right)\right)\right)$
17 0 16 wceq ${wff}{+}_{\mathrm{fn}}=\left({f}\in \left({ℂ}^{ℋ}\right),{g}\in \left({ℂ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}\left({x}\right)+{g}\left({x}\right)\right)\right)$