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	⊢ +fn = ( 𝑓 ∈ ( ℂ ↑m ℋ ) , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chfs	⊢ +fn
1		vf	⊢ 𝑓
2		cc	⊢ ℂ
3		cmap	⊢ ↑m
4		chba	⊢ ℋ
5	2 4 3	co	⊢ ( ℂ ↑m ℋ )
6		vg	⊢ 𝑔
7		vx	⊢ 𝑥
8	1	cv	⊢ 𝑓
9	7	cv	⊢ 𝑥
10	9 8	cfv	⊢ ( 𝑓 ‘ 𝑥 )
11		caddc	⊢ +
12	6	cv	⊢ 𝑔
13	9 12	cfv	⊢ ( 𝑔 ‘ 𝑥 )
14	10 13 11	co	⊢ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) )
15	7 4 14	cmpt	⊢ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) )
16	1 6 5 5 15	cmpo	⊢ ( 𝑓 ∈ ( ℂ ↑m ℋ ) , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) )
17	0 16	wceq	⊢ +fn = ( 𝑓 ∈ ( ℂ ↑m ℋ ) , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) )