Definition df-hfsum 9426

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 ℋ to ℂ, not just linear (or bounded linear) ones.

Assertion

Ref	Expression
df-hfsum	⊢ +fn = {⟨⟨f, g⟩, h⟩∣((f: ℋ –→ℂ ⋀ g: ℋ –→ℂ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) + (g ‘x)))})}

Distinct variable group:   f,g,h,x,y

Detailed syntax breakdown of Definition df-hfsum

Step	Hyp	Ref	Expression
1		chfs 8749	. 2 class +fn
2		chil 8727	. . . . . 6 class ℋ
3		cc 5204	. . . . . 6 class ℂ
4		vf	. . . . . . 7 set f
5	4	cv 952	. . . . . 6 class f
6	2, 3, 5	wf 3168	. . . . 5 wff f: ℋ –→ℂ
7		vg	. . . . . . 7 set g
8	7	cv 952	. . . . . 6 class g
9	2, 3, 8	wf 3168	. . . . 5 wff g: ℋ –→ℂ
10	6, 9	wa 223	. . . 4 wff (f: ℋ –→ℂ ⋀ g: ℋ –→ℂ)
11		vh	. . . . . 6 set h
12	11	cv 952	. . . . 5 class h
13		vx	. . . . . . . . 9 set x
14	13	cv 952	. . . . . . . 8 class x
15	14, 2	wcel 955	. . . . . . 7 wff x ∈ ℋ
16		vy	. . . . . . . . 9 set y
17	16	cv 952	. . . . . . . 8 class y
18	14, 5	cfv 3172	. . . . . . . . 9 class (f ‘x)
19	14, 8	cfv 3172	. . . . . . . . 9 class (g ‘x)
20		caddc 5209	. . . . . . . . 9 class +
21	18, 19, 20	co 3948	. . . . . . . 8 class ((f ‘x) + (g ‘x))
22	17, 21	wceq 953	. . . . . . 7 wff y = ((f ‘x) + (g ‘x))
23	15, 22	wa 223	. . . . . 6 wff (x ∈ ℋ ⋀ y = ((f ‘x) + (g ‘x)))
24	23, 13, 16	copab 2656	. . . . 5 class {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) + (g ‘x)))}
25	12, 24	wceq 953	. . . 4 wff h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) + (g ‘x)))}
26	10, 25	wa 223	. . 3 wff ((f: ℋ –→ℂ ⋀ g: ℋ –→ℂ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) + (g ‘x)))})
27	26, 4, 7, 11	copab2 3949	. 2 class {⟨⟨f, g⟩, h⟩∣((f: ℋ –→ℂ ⋀ g: ℋ –→ℂ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) + (g ‘x)))})}
28	1, 27	wceq 953	1 wff +fn = {⟨⟨f, g⟩, h⟩∣((f: ℋ –→ℂ ⋀ g: ℋ –→ℂ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) + (g ‘x)))})}

This definition is referenced by:  hfsmvalt 9431

Copyright terms: Public domain