Definition df-eigval 9720

Description: Define the eigenvalue function. The range of eigval ‘T is the set of eigenvalues of Hilbert space operator T. Theorem eigvalclt 9824 shows that (eigval ‘T) ‘A, the eigenvalue associated with eigenvector A, is a complex number.

Assertion

Ref	Expression
df-eigval	⊢ eigval = {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = {⟨x, z⟩∣(x ∈ (eigvec ‘t) ⋀ z = (((t ‘x) ·ih x) / ((normh ‘x)↑2)))})}

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-eigval

Step	Hyp	Ref	Expression
1		cel 8768	. 2 class eigval
2		chil 8727	. . . . 5 class ℋ
3		vt	. . . . . 6 set t
4	3	cv 953	. . . . 5 class t
5	2, 2, 4	wf 3173	. . . 4 wff t: ℋ –→ ℋ
6		vy	. . . . . 6 set y
7	6	cv 953	. . . . 5 class y
8		vx	. . . . . . . . 9 set x
9	8	cv 953	. . . . . . . 8 class x
10		cei 8767	. . . . . . . . 9 class eigvec
11	4, 10	cfv 3177	. . . . . . . 8 class (eigvec ‘t)
12	9, 11	wcel 956	. . . . . . 7 wff x ∈ (eigvec ‘t)
13		vz	. . . . . . . . 9 set z
14	13	cv 953	. . . . . . . 8 class z
15	9, 4	cfv 3177	. . . . . . . . . 10 class (t ‘x)
16		csp 8732	. . . . . . . . . 10 class ·ih
17	15, 9, 16	co 3954	. . . . . . . . 9 class ((t ‘x) ·ih x)
18		cno 8733	. . . . . . . . . . 11 class normh
19	9, 18	cfv 3177	. . . . . . . . . 10 class (normh ‘x)
20		c2 5916	. . . . . . . . . 10 class 2
21		cexp 6508	. . . . . . . . . 10 class ↑
22	19, 20, 21	co 3954	. . . . . . . . 9 class ((normh ‘x)↑2)
23		cdiv 5274	. . . . . . . . 9 class /
24	17, 22, 23	co 3954	. . . . . . . 8 class (((t ‘x) ·ih x) / ((normh ‘x)↑2))
25	14, 24	wceq 954	. . . . . . 7 wff z = (((t ‘x) ·ih x) / ((normh ‘x)↑2))
26	12, 25	wa 223	. . . . . 6 wff (x ∈ (eigvec ‘t) ⋀ z = (((t ‘x) ·ih x) / ((normh ‘x)↑2)))
27	26, 8, 13	copab 2661	. . . . 5 class {⟨x, z⟩∣(x ∈ (eigvec ‘t) ⋀ z = (((t ‘x) ·ih x) / ((normh ‘x)↑2)))}
28	7, 27	wceq 954	. . . 4 wff y = {⟨x, z⟩∣(x ∈ (eigvec ‘t) ⋀ z = (((t ‘x) ·ih x) / ((normh ‘x)↑2)))}
29	5, 28	wa 223	. . 3 wff (t: ℋ –→ ℋ ⋀ y = {⟨x, z⟩∣(x ∈ (eigvec ‘t) ⋀ z = (((t ‘x) ·ih x) / ((normh ‘x)↑2)))})
30	29, 3, 6	copab 2661	. 2 class {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = {⟨x, z⟩∣(x ∈ (eigvec ‘t) ⋀ z = (((t ‘x) ·ih x) / ((normh ‘x)↑2)))})}
31	1, 30	wceq 954	1 wff eigval = {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = {⟨x, z⟩∣(x ∈ (eigvec ‘t) ⋀ z = (((t ‘x) ·ih x) / ((normh ‘x)↑2)))})}

This definition is referenced by:  eigvalvalt 9763

Copyright terms: Public domain