Definition df-eigvec

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cei	|- eigvec
1		vt	|- t
2		chba	|- ~H
3		cmap	|- ^m
4	2 2 3	co	|- ( ~H ^m ~H )
5		vx	|- x
6		c0h	|- 0H
7	2 6	cdif	|- ( ~H \ 0H )
8		vz	|- z
9		cc	|- CC
10	1	cv	|- t
11	5	cv	|- x
12	11 10	cfv	|- ( t ` x )
13	8	cv	|- z
14		csm	|- .h
15	13 11 14	co	|- ( z .h x )
16	12 15	wceq	|- ( t ` x ) = ( z .h x )
17	16 8 9	wrex	|- E. z e. CC ( t ` x ) = ( z .h x )
18	17 5 7	crab	|- { x e. ( ~H \ 0H ) | E. z e. CC ( t ` x ) = ( z .h x ) }
19	1 4 18	cmpt	|- ( t e. ( ~H ^m ~H ) |-> { x e. ( ~H \ 0H ) | E. z e. CC ( t ` x ) = ( z .h x ) } )
20	0 19	wceq	|- eigvec = ( t e. ( ~H ^m ~H ) |-> { x e. ( ~H \ 0H ) | E. z e. CC ( t ` x ) = ( z .h x ) } )