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({ℂ}^{\mathscr{H}}\right),g\in \left({ℂ}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f\left(x\right)+g\left(x\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chfs	$$class{+}_{\mathrm{fn}}$$
1		vf	$$setvarf$$
2		cc	$$classℂ$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		chba	$$class\mathscr{H}$$
5	2 4 3	co	$$class\left({ℂ}^{\mathscr{H}}\right)$$
6		vg	$$setvarg$$
7		vx	$$setvarx$$
8	1	cv	$$setvarf$$
9	7	cv	$$setvarx$$
10	9 8	cfv	$$classf\left(x\right)$$
11		caddc	$$class+$$
12	6	cv	$$setvarg$$
13	9 12	cfv	$$classg\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 \mathscr{H}⟼f\left(x\right)+g\left(x\right)\right)$$
16	1 6 5 5 15	cmpo	$$class\left(f\in \left({ℂ}^{\mathscr{H}}\right),g\in \left({ℂ}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f\left(x\right)+g\left(x\right)\right)\right)$$
17	0 16	wceq	$$wff{+}_{\mathrm{fn}}=\left(f\in \left({ℂ}^{\mathscr{H}}\right),g\in \left({ℂ}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f\left(x\right)+g\left(x\right)\right)\right)$$