Definition df-eigvec 28096

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

Assertion

Ref	Expression
df-eigvec	⊢ eigvec = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)})

Distinct variable group:   𝑥,𝑡,𝑧

Detailed syntax breakdown of Definition df-eigvec

Step	Hyp	Ref	Expression
1		cei 27200	. 2 class eigvec
2		vt	. . 3 setvar 𝑡
3		chil 27160	. . . 4 class ℋ
4		cmap 7744	. . . 4 class ↑𝑚
5	3, 3, 4	co 6549	. . 3 class ( ℋ ↑𝑚 ℋ)
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1474	. . . . . . 7 class 𝑥
8	2	cv 1474	. . . . . . 7 class 𝑡
9	7, 8	cfv 5804	. . . . . 6 class (𝑡‘𝑥)
10		vz	. . . . . . . 8 setvar 𝑧
11	10	cv 1474	. . . . . . 7 class 𝑧
12		csm 27162	. . . . . . 7 class ·ℎ
13	11, 7, 12	co 6549	. . . . . 6 class (𝑧 ·ℎ 𝑥)
14	9, 13	wceq 1475	. . . . 5 wff (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)
15		cc 9813	. . . . 5 class ℂ
16	14, 10, 15	wrex 2897	. . . 4 wff ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)
17		c0h 27176	. . . . 5 class 0ℋ
18	3, 17	cdif 3537	. . . 4 class ( ℋ ∖ 0ℋ)
19	16, 6, 18	crab 2900	. . 3 class {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)}
20	2, 5, 19	cmpt 4643	. 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)})
21	1, 20	wceq 1475	1 wff eigvec = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ {𝑥 ∈ ( ℋ ∖ 0ℋ) ∣ ∃𝑧 ∈ ℂ (𝑡‘𝑥) = (𝑧 ·ℎ 𝑥)})

This definition is referenced by:  eigvecval  28139