This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ ℋ ℋ ⟼ x ∈ ℋ ∖ 0 ℋ | ∃ z ∈ ℂ t ⁡ x = z ⋅ ℎ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cei class eigvec
1 vt setvar t
2 chba class ℋ
3 cmap class ↑ 𝑚
4 2 2 3 co class ℋ ℋ
5 vx setvar x
6 c0h class 0 ℋ
7 2 6 cdif class ℋ ∖ 0 ℋ
8 vz setvar z
9 cc class ℂ
10 1 cv setvar t
11 5 cv setvar x
12 11 10 cfv class t ⁡ x
13 8 cv setvar z
14 csm class ⋅ ℎ
15 13 11 14 co class z ⋅ ℎ x
16 12 15 wceq wff t ⁡ x = z ⋅ ℎ x
17 16 8 9 wrex wff ∃ z ∈ ℂ t ⁡ x = z ⋅ ℎ x
18 17 5 7 crab class x ∈ ℋ ∖ 0 ℋ | ∃ z ∈ ℂ t ⁡ x = z ⋅ ℎ x
19 1 4 18 cmpt class t ∈ ℋ ℋ ⟼ x ∈ ℋ ∖ 0 ℋ | ∃ z ∈ ℂ t ⁡ x = z ⋅ ℎ x
20 0 19 wceq wff eigvec = t ∈ ℋ ℋ ⟼ x ∈ ℋ ∖ 0 ℋ | ∃ z ∈ ℂ t ⁡ x = z ⋅ ℎ x