Definition df-lnop 9752

Description: Define the set of linear operators on Hilbert space. (See df-hosum 9491 for definition of operator.)

Assertion

Ref	Expression
df-lnop	⊢ LinOp = {t∣(t: ℋ –→ ℋ ⋀ ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x ·h (t ‘y)) +h (t ‘z)))}

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-lnop

Step	Hyp	Ref	Expression
1		clo 8801	. 2 class LinOp
2		chil 8773	. . . . 5 class ℋ
3		vt	. . . . . 6 set t
4	3	cv 955	. . . . 5 class t
5	2, 2, 4	wf 3178	. . . 4 wff t: ℋ –→ ℋ
6		vx	. . . . . . . . . . . 12 set x
7	6	cv 955	. . . . . . . . . . 11 class x
8		vy	. . . . . . . . . . . 12 set y
9	8	cv 955	. . . . . . . . . . 11 class y
10		csm 8775	. . . . . . . . . . 11 class ·h
11	7, 9, 10	co 3963	. . . . . . . . . 10 class (x ·h y)
12		vz	. . . . . . . . . . 11 set z
13	12	cv 955	. . . . . . . . . 10 class z
14		cva 8774	. . . . . . . . . 10 class +h
15	11, 13, 14	co 3963	. . . . . . . . 9 class ((x ·h y) +h z)
16	15, 4	cfv 3182	. . . . . . . 8 class (t ‘((x ·h y) +h z))
17	9, 4	cfv 3182	. . . . . . . . . 10 class (t ‘y)
18	7, 17, 10	co 3963	. . . . . . . . 9 class (x ·h (t ‘y))
19	13, 4	cfv 3182	. . . . . . . . 9 class (t ‘z)
20	18, 19, 14	co 3963	. . . . . . . 8 class ((x ·h (t ‘y)) +h (t ‘z))
21	16, 20	wceq 956	. . . . . . 7 wff (t ‘((x ·h y) +h z)) = ((x ·h (t ‘y)) +h (t ‘z))
22	21, 12, 2	wral 1645	. . . . . 6 wff ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x ·h (t ‘y)) +h (t ‘z))
23	22, 8, 2	wral 1645	. . . . 5 wff ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x ·h (t ‘y)) +h (t ‘z))
24		cc 5224	. . . . 5 class ℂ
25	23, 6, 24	wral 1645	. . . 4 wff ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x ·h (t ‘y)) +h (t ‘z))
26	5, 25	wa 223	. . 3 wff (t: ℋ –→ ℋ ⋀ ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x ·h (t ‘y)) +h (t ‘z)))
27	26, 3	cab 1463	. 2 class {t∣(t: ℋ –→ ℋ ⋀ ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x ·h (t ‘y)) +h (t ‘z)))}
28	1, 27	wceq 956	1 wff LinOp = {t∣(t: ℋ –→ ℋ ⋀ ∀x ∈ ℂ ∀y ∈ ℋ ∀z ∈ ℋ (t ‘((x ·h y) +h z)) = ((x ·h (t ‘y)) +h (t ‘z)))}

This definition is referenced by:  ellnopt 9769  hhlno 9811

Copyright terms: Public domain