df-spec

Description: Define the spectrum of an operator. Definition of spectrum in Halmos p. 50. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-spec	$⊢ Lambda = (t \in (ℋ^{ℋ}) ⟼ \{x \in ℂ \| \neg (t -_{op} (x \cdot_{op} ({I ↾}_{ℋ}))) : ℋ \underset{1-1}{⟶} ℋ\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspc	$class Lambda$
1		vt	$setvar t$
2		chba	$class ℋ$
3		cmap	$class ↑_{𝑚}$
4	2 2 3	co	$class (ℋ^{ℋ})$
5		vx	$setvar x$
6		cc	$class ℂ$
7	1	cv	$setvar t$
8		chod	$class -_{op}$
9	5	cv	$setvar x$
10		chot	$class \cdot_{op}$
11		cid	$class I$
12	11 2	cres	$class ({I ↾}_{ℋ})$
13	9 12 10	co	$class (x \cdot_{op} ({I ↾}_{ℋ}))$
14	7 13 8	co	$class (t -_{op} (x \cdot_{op} ({I ↾}_{ℋ})))$
15	2 2 14	wf1	$wff (t -_{op} (x \cdot_{op} ({I ↾}_{ℋ}))) : ℋ \underset{1-1}{⟶} ℋ$
16	15	wn	$wff \neg (t -_{op} (x \cdot_{op} ({I ↾}_{ℋ}))) : ℋ \underset{1-1}{⟶} ℋ$
17	16 5 6	crab	$class \{x \in ℂ \| \neg (t -_{op} (x \cdot_{op} ({I ↾}_{ℋ}))) : ℋ \underset{1-1}{⟶} ℋ\}$
18	1 4 17	cmpt	$class (t \in (ℋ^{ℋ}) ⟼ \{x \in ℂ \| \neg (t -_{op} (x \cdot_{op} ({I ↾}_{ℋ}))) : ℋ \underset{1-1}{⟶} ℋ\})$
19	0 18	wceq	$wff Lambda = (t \in (ℋ^{ℋ}) ⟼ \{x \in ℂ \| \neg (t -_{op} (x \cdot_{op} ({I ↾}_{ℋ}))) : ℋ \underset{1-1}{⟶} ℋ\})$

Metamath Proof Explorer

Definition df-spec

Detailed syntax breakdown