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

Metamath Proof Explorer

Definition df-eigval

Description: Define the eigenvalue function. The range of eigvalT is the set of eigenvalues of Hilbert space operator T . Theorem eigvalcl shows that ( eigvalT )A , the eigenvalue associated with eigenvector A , is a complex number. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion df-eigval ⊢ eigval = t ∈ ℋ ℋ ⟼ x ∈ eigvec ⁡ t ⟼ t ⁡ x ⋅ ih x norm ℎ ⁡ x 2

Detailed syntax breakdown

Step Hyp Ref Expression
0 cel class eigval
1 vt setvar t
2 chba class ℋ
3 cmap class ↑ 𝑚
4 2 2 3 co class ℋ ℋ
5 vx setvar x
6 cei class eigvec
7 1 cv setvar t
8 7 6 cfv class eigvec ⁡ t
9 5 cv setvar x
10 9 7 cfv class t ⁡ x
11 csp class ⋅ ih
12 10 9 11 co class t ⁡ x ⋅ ih x
13 cdiv class ÷
14 cno class norm ℎ
15 9 14 cfv class norm ℎ ⁡ x
16 cexp class ^
17 c2 class 2
18 15 17 16 co class norm ℎ ⁡ x 2
19 12 18 13 co class t ⁡ x ⋅ ih x norm ℎ ⁡ x 2
20 5 8 19 cmpt class x ∈ eigvec ⁡ t ⟼ t ⁡ x ⋅ ih x norm ℎ ⁡ x 2
21 1 4 20 cmpt class t ∈ ℋ ℋ ⟼ x ∈ eigvec ⁡ t ⟼ t ⁡ x ⋅ ih x norm ℎ ⁡ x 2
22 0 21 wceq wff eigval = t ∈ ℋ ℋ ⟼ x ∈ eigvec ⁡ t ⟼ t ⁡ x ⋅ ih x norm ℎ ⁡ x 2