Definition df-hosum 9446

Description: Define the sum of two Hilbert space operators. Definition of [Beran] p. 111.

Note on operators. Unlike some authors, we use the term "operator" to mean any function from ℋ to ℋ. This is the definition of operator in [Hughes] p. 14, the definition of operator in [AkhiezerGlazman] p. 30, and the definition of operator in [Goldberg] p. 10. For Reed and Simon, an operator is linear (definition of operator in [ReedSimon] p. 2). For Halmos, an operator is bounded and linear (definition of operator in [Halmos] p. 35). For Kalmbach and Beran, an operator is continuous and linear (definition of operator in [Kalmbach] p. 353; definition of operator in [Beran] p. 99). Note that "bounded and linear" and "continuous and linear" are equivalent by lncnbd 9905.

Assertion

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

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

Detailed syntax breakdown of Definition df-hosum

Step	Hyp	Ref	Expression
1		chos 8746	. 2 class +op
2		chil 8727	. . . . . 6 class ℋ
3		vf	. . . . . . 7 set f
4	3	cv 953	. . . . . 6 class f
5	2, 2, 4	wf 3173	. . . . 5 wff f: ℋ –→ ℋ
6		vg	. . . . . . 7 set g
7	6	cv 953	. . . . . 6 class g
8	2, 2, 7	wf 3173	. . . . 5 wff g: ℋ –→ ℋ
9	5, 8	wa 223	. . . 4 wff (f: ℋ –→ ℋ ⋀ g: ℋ –→ ℋ )
10		vh	. . . . . 6 set h
11	10	cv 953	. . . . 5 class h
12		vx	. . . . . . . . 9 set x
13	12	cv 953	. . . . . . . 8 class x
14	13, 2	wcel 956	. . . . . . 7 wff x ∈ ℋ
15		vy	. . . . . . . . 9 set y
16	15	cv 953	. . . . . . . 8 class y
17	13, 4	cfv 3177	. . . . . . . . 9 class (f ‘x)
18	13, 7	cfv 3177	. . . . . . . . 9 class (g ‘x)
19		cva 8728	. . . . . . . . 9 class +h
20	17, 18, 19	co 3954	. . . . . . . 8 class ((f ‘x) +h (g ‘x))
21	16, 20	wceq 954	. . . . . . 7 wff y = ((f ‘x) +h (g ‘x))
22	14, 21	wa 223	. . . . . 6 wff (x ∈ ℋ ⋀ y = ((f ‘x) +h (g ‘x)))
23	22, 12, 15	copab 2661	. . . . 5 class {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) +h (g ‘x)))}
24	11, 23	wceq 954	. . . 4 wff h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) +h (g ‘x)))}
25	9, 24	wa 223	. . 3 wff ((f: ℋ –→ ℋ ⋀ g: ℋ –→ ℋ ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) +h (g ‘x)))})
26	25, 3, 6, 10	copab2 3955	. 2 class {⟨⟨f, g⟩, h⟩∣((f: ℋ –→ ℋ ⋀ g: ℋ –→ ℋ ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) +h (g ‘x)))})}
27	1, 26	wceq 954	1 wff +op = {⟨⟨f, g⟩, h⟩∣((f: ℋ –→ ℋ ⋀ g: ℋ –→ ℋ ) ⋀ h = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = ((f ‘x) +h (g ‘x)))})}

This definition is referenced by:  hosmvalt 9451

Copyright terms: Public domain