Metamath Proof Explorer


Theorem nmopsetretHIL

Description: The set in the supremum of the operator norm definition df-nmop is a set of reals. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopsetretHIL ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ { ๐‘ฅ โˆฃ โˆƒ ๐‘ฆ โˆˆ โ„‹ ( ( normโ„Ž โ€˜ ๐‘ฆ ) โ‰ค 1 โˆง ๐‘ฅ = ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) ) } โŠ† โ„ )

Proof

Step Hyp Ref Expression
1 eqid โŠข โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 1 hhnv โŠข โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ โˆˆ NrmCVec
3 df-hba โŠข โ„‹ = ( BaseSet โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ )
4 1 hhnm โŠข normโ„Ž = ( normCV โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ )
5 3 4 nmosetre โŠข ( ( โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ โˆˆ NrmCVec โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ { ๐‘ฅ โˆฃ โˆƒ ๐‘ฆ โˆˆ โ„‹ ( ( normโ„Ž โ€˜ ๐‘ฆ ) โ‰ค 1 โˆง ๐‘ฅ = ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) ) } โŠ† โ„ )
6 2 5 mpan โŠข ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ { ๐‘ฅ โˆฃ โˆƒ ๐‘ฆ โˆˆ โ„‹ ( ( normโ„Ž โ€˜ ๐‘ฆ ) โ‰ค 1 โˆง ๐‘ฅ = ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) ) } โŠ† โ„ )