Metamath Proof Explorer

Theorem speccl

Description: The spectrum of an operator is a set of complex numbers. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion speccl ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ ( Lambda โ€˜ ๐‘‡ ) โŠ† โ„‚ )

Proof

Step Hyp Ref Expression
1 specval โŠข ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ ( Lambda โ€˜ ๐‘‡ ) = { ๐‘ฅ โˆˆ โ„‚ โˆฃ ยฌ ( ๐‘‡ โˆ’op ( ๐‘ฅ ยทop ( I โ†พ โ„‹ ) ) ) : โ„‹ โ€“1-1โ†’ โ„‹ } )
2 ssrab2 โŠข { ๐‘ฅ โˆˆ โ„‚ โˆฃ ยฌ ( ๐‘‡ โˆ’op ( ๐‘ฅ ยทop ( I โ†พ โ„‹ ) ) ) : โ„‹ โ€“1-1โ†’ โ„‹ } โŠ† โ„‚
3 1 2 eqsstrdi โŠข ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ ( Lambda โ€˜ ๐‘‡ ) โŠ† โ„‚ )