Definition df-eigvec 28712

Description: Define the eigenvector function. Theorem eleigveccl 28818 shows that eigvec ` T, the set of eigenvectors of Hilbert space operator T, are Hilbert space vectors. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-eigvec	|- eigvec = ( t e. ( ~H ^m ~H ) |-> { x e. ( ~H \ 0H ) | E. z e. CC ( t ` x ) = ( z .h x ) } )

Distinct variable group:   x, t, z

Detailed syntax breakdown of Definition df-eigvec

Step	Hyp	Ref	Expression
1		cei 27816	. 2 class eigvec
2		vt	. . 3 setvar t
3		chil 27776	. . . 4 class ~H
4		cmap 7857	. . . 4 class ^m
5	3, 3, 4	co 6650	. . 3 class ( ~H ^m ~H )
6		vx	. . . . . . . 8 setvar x
7	6	cv 1482	. . . . . . 7 class x
8	2	cv 1482	. . . . . . 7 class t
9	7, 8	cfv 5888	. . . . . 6 class ( t ` x )
10		vz	. . . . . . . 8 setvar z
11	10	cv 1482	. . . . . . 7 class z
12		csm 27778	. . . . . . 7 class .h
13	11, 7, 12	co 6650	. . . . . 6 class ( z .h x )
14	9, 13	wceq 1483	. . . . 5 wff ( t ` x ) = ( z .h x )
15		cc 9934	. . . . 5 class CC
16	14, 10, 15	wrex 2913	. . . 4 wff E. z e. CC ( t ` x ) = ( z .h x )
17		c0h 27792	. . . . 5 class 0H
18	3, 17	cdif 3571	. . . 4 class ( ~H \ 0H )
19	16, 6, 18	crab 2916	. . 3 class { x e. ( ~H \ 0H ) | E. z e. CC ( t ` x ) = ( z .h x ) }
20	2, 5, 19	cmpt 4729	. 2 class ( t e. ( ~H ^m ~H ) |-> { x e. ( ~H \ 0H ) | E. z e. CC ( t ` x ) = ( z .h x ) } )
21	1, 20	wceq 1483	1 wff eigvec = ( t e. ( ~H ^m ~H ) |-> { x e. ( ~H \ 0H ) | E. z e. CC ( t ` x ) = ( z .h x ) } )

This definition is referenced by:  eigvecval  28755