Metamath Proof Explorer

Theorem hhbloi

Description: A bounded linear operator in Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses hhnmo.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
hhblo.2 โŠข ๐ต = ( ๐‘ˆ BLnOp ๐‘ˆ )
Assertion hhbloi BndLinOp = ๐ต

Proof

Step Hyp Ref Expression
1 hhnmo.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 hhblo.2 โŠข ๐ต = ( ๐‘ˆ BLnOp ๐‘ˆ )
3 df-bdop โŠข BndLinOp = { ๐‘ฅ โˆˆ LinOp โˆฃ ( normop โ€˜ ๐‘ฅ ) < +โˆž }
4 1 hhnv โŠข ๐‘ˆ โˆˆ NrmCVec
5 eqid โŠข ( ๐‘ˆ normOpOLD ๐‘ˆ ) = ( ๐‘ˆ normOpOLD ๐‘ˆ )
6 1 5 hhnmoi โŠข normop = ( ๐‘ˆ normOpOLD ๐‘ˆ )
7 eqid โŠข ( ๐‘ˆ LnOp ๐‘ˆ ) = ( ๐‘ˆ LnOp ๐‘ˆ )
8 1 7 hhlnoi โŠข LinOp = ( ๐‘ˆ LnOp ๐‘ˆ )
9 6 8 2 bloval โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘ˆ โˆˆ NrmCVec ) โ†’ ๐ต = { ๐‘ฅ โˆˆ LinOp โˆฃ ( normop โ€˜ ๐‘ฅ ) < +โˆž } )
10 4 4 9 mp2an โŠข ๐ต = { ๐‘ฅ โˆˆ LinOp โˆฃ ( normop โ€˜ ๐‘ฅ ) < +โˆž }
11 3 10 eqtr4i โŠข BndLinOp = ๐ต