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 = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 ·ℎ 𝑥 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cei	⊢ eigvec
1		vt	⊢ 𝑡
2		chba	⊢ ℋ
3		cmap	⊢ ↑m
4	2 2 3	co	⊢ ( ℋ ↑m ℋ )
5		vx	⊢ 𝑥
6		c0h	⊢ 0ℋ
7	2 6	cdif	⊢ ( ℋ ∖ 0ℋ )
8		vz	⊢ 𝑧
9		cc	⊢ ℂ
10	1	cv	⊢ 𝑡
11	5	cv	⊢ 𝑥
12	11 10	cfv	⊢ ( 𝑡 ‘ 𝑥 )
13	8	cv	⊢ 𝑧
14		csm	⊢ ·ℎ
15	13 11 14	co	⊢ ( 𝑧 ·ℎ 𝑥 )
16	12 15	wceq	⊢ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 ·ℎ 𝑥 )
17	16 8 9	wrex	⊢ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 ·ℎ 𝑥 )
18	17 5 7	crab	⊢ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 ·ℎ 𝑥 ) }
19	1 4 18	cmpt	⊢ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 ·ℎ 𝑥 ) } )
20	0 19	wceq	⊢ eigvec = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↦ { 𝑥 ∈ ( ℋ ∖ 0ℋ ) ∣ ∃ 𝑧 ∈ ℂ ( 𝑡 ‘ 𝑥 ) = ( 𝑧 ·ℎ 𝑥 ) } )