Definition df-eigval 9735

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

Assertion

Ref	Expression
df-eigval	|- eigval = {<.t, y>. | (t:H~-->H~ /\ y = {<.x, z>. | (x e. (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 8784	. 2 class eigval
2		chil 8743	. . . . 5 class H~
3		vt	. . . . . 6 set t
4	3	cv 955	. . . . 5 class t
5	2, 2, 4	wf 3176	. . . 4 wff t:H~-->H~
6		vy	. . . . . 6 set y
7	6	cv 955	. . . . 5 class y
8		vx	. . . . . . . . 9 set x
9	8	cv 955	. . . . . . . 8 class x
10		cei 8783	. . . . . . . . 9 class eigvec
11	4, 10	cfv 3180	. . . . . . . 8 class (eigvec` t)
12	9, 11	wcel 958	. . . . . . 7 wff x e. (eigvec` t)
13		vz	. . . . . . . . 9 set z
14	13	cv 955	. . . . . . . 8 class z
15	9, 4	cfv 3180	. . . . . . . . . 10 class (t` x)
16		csp 8748	. . . . . . . . . 10 class .ih
17	15, 9, 16	co 3961	. . . . . . . . 9 class ((t` x) .ih x)
18		cno 8749	. . . . . . . . . . 11 class normh
19	9, 18	cfv 3180	. . . . . . . . . 10 class (normh` x)
20		c2 5929	. . . . . . . . . 10 class 2
21		cexp 6528	. . . . . . . . . 10 class ^
22	19, 20, 21	co 3961	. . . . . . . . 9 class ((normh` x)^2)
23		cdiv 5282	. . . . . . . . 9 class /
24	17, 22, 23	co 3961	. . . . . . . 8 class (((t` x) .ih x) / ((normh` x)^2))
25	14, 24	wceq 956	. . . . . . 7 wff z = (((t` x) .ih x) / ((normh` x)^2))
26	12, 25	wa 223	. . . . . 6 wff (x e. (eigvec` t) /\ z = (((t` x) .ih x) / ((normh` x)^2)))
27	26, 8, 13	copab 2664	. . . . 5 class {<.x, z>. | (x e. (eigvec` t) /\ z = (((t` x) .ih x) / ((normh` x)^2)))}
28	7, 27	wceq 956	. . . 4 wff y = {<.x, z>. | (x e. (eigvec` t) /\ z = (((t` x) .ih x) / ((normh` x)^2)))}
29	5, 28	wa 223	. . 3 wff (t:H~-->H~ /\ y = {<.x, z>. | (x e. (eigvec` t) /\ z = (((t` x) .ih x) / ((normh` x)^2)))})
30	29, 3, 6	copab 2664	. 2 class {<.t, y>. | (t:H~-->H~ /\ y = {<.x, z>. | (x e. (eigvec` t) /\ z = (((t` x) .ih x) / ((normh` x)^2)))})}
31	1, 30	wceq 956	1 wff eigval = {<.t, y>. | (t:H~-->H~ /\ y = {<.x, z>. | (x e. (eigvec` t) /\ z = (((t` x) .ih x) / ((normh` x)^2)))})}

This definition is referenced by:  eigvalvalt 9778

Copyright terms: Public domain