Definition df-eigvec 9696

Description: Define the eigenvector function. Theorem eleigvecclt 9799 shows that eigvec ‘T, the set of eigenvectors of Hilbert space operator T, are Hilbert space vectors.

Assertion

Ref	Expression
df-eigvec	⊢ eigvec = {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = {x ∈ ℋ ∣(x ≠ 0h ⋀ ∃z ∈ ℂ (t ‘x) = (z ·h x))})}

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-eigvec

Step	Hyp	Ref	Expression
1		cei 8767	. 2 class eigvec
2		chil 8727	. . . . 5 class ℋ
3		vt	. . . . . 6 set t
4	3	cv 952	. . . . 5 class t
5	2, 2, 4	wf 3168	. . . 4 wff t: ℋ –→ ℋ
6		vy	. . . . . 6 set y
7	6	cv 952	. . . . 5 class y
8		vx	. . . . . . . . 9 set x
9	8	cv 952	. . . . . . . 8 class x
10		c0v 8730	. . . . . . . 8 class 0h
11	9, 10	wne 1577	. . . . . . 7 wff x ≠ 0h
12	9, 4	cfv 3172	. . . . . . . . 9 class (t ‘x)
13		vz	. . . . . . . . . . 11 set z
14	13	cv 952	. . . . . . . . . 10 class z
15		csm 8729	. . . . . . . . . 10 class ·h
16	14, 9, 15	co 3948	. . . . . . . . 9 class (z ·h x)
17	12, 16	wceq 953	. . . . . . . 8 wff (t ‘x) = (z ·h x)
18		cc 5204	. . . . . . . 8 class ℂ
19	17, 13, 18	wrex 1638	. . . . . . 7 wff ∃z ∈ ℂ (t ‘x) = (z ·h x)
20	11, 19	wa 223	. . . . . 6 wff (x ≠ 0h ⋀ ∃z ∈ ℂ (t ‘x) = (z ·h x))
21	20, 8, 2	crab 1640	. . . . 5 class {x ∈ ℋ ∣(x ≠ 0h ⋀ ∃z ∈ ℂ (t ‘x) = (z ·h x))}
22	7, 21	wceq 953	. . . 4 wff y = {x ∈ ℋ ∣(x ≠ 0h ⋀ ∃z ∈ ℂ (t ‘x) = (z ·h x))}
23	5, 22	wa 223	. . 3 wff (t: ℋ –→ ℋ ⋀ y = {x ∈ ℋ ∣(x ≠ 0h ⋀ ∃z ∈ ℂ (t ‘x) = (z ·h x))})
24	23, 3, 6	copab 2656	. 2 class {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = {x ∈ ℋ ∣(x ≠ 0h ⋀ ∃z ∈ ℂ (t ‘x) = (z ·h x))})}
25	1, 24	wceq 953	1 wff eigvec = {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = {x ∈ ℋ ∣(x ≠ 0h ⋀ ∃z ∈ ℂ (t ‘x) = (z ·h x))})}

This definition is referenced by:  eigvecvalt 9739

Copyright terms: Public domain