Metamath Proof Explorer


Theorem lnopcnbd

Description: A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopcnbd ( ๐‘‡ โˆˆ LinOp โ†’ ( ๐‘‡ โˆˆ ContOp โ†” ๐‘‡ โˆˆ BndLinOp ) )

Proof

Step Hyp Ref Expression
1 nmcopex โŠข ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ โˆˆ ContOp ) โ†’ ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ )
2 1 ex โŠข ( ๐‘‡ โˆˆ LinOp โ†’ ( ๐‘‡ โˆˆ ContOp โ†’ ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ ) )
3 elbdop2 โŠข ( ๐‘‡ โˆˆ BndLinOp โ†” ( ๐‘‡ โˆˆ LinOp โˆง ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ ) )
4 3 baibr โŠข ( ๐‘‡ โˆˆ LinOp โ†’ ( ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ โ†” ๐‘‡ โˆˆ BndLinOp ) )
5 2 4 sylibd โŠข ( ๐‘‡ โˆˆ LinOp โ†’ ( ๐‘‡ โˆˆ ContOp โ†’ ๐‘‡ โˆˆ BndLinOp ) )
6 nmopre โŠข ( ๐‘‡ โˆˆ BndLinOp โ†’ ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ )
7 nmbdoplb โŠข ( ( ๐‘‡ โˆˆ BndLinOp โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
8 7 ralrimiva โŠข ( ๐‘‡ โˆˆ BndLinOp โ†’ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
9 oveq1 โŠข ( ๐‘ฅ = ( normop โ€˜ ๐‘‡ ) โ†’ ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) = ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
10 9 breq2d โŠข ( ๐‘ฅ = ( normop โ€˜ ๐‘‡ ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) โ†” ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) ) )
11 10 ralbidv โŠข ( ๐‘ฅ = ( normop โ€˜ ๐‘‡ ) โ†’ ( โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) โ†” โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) ) )
12 11 rspcev โŠข ( ( ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ โˆง โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
13 6 8 12 syl2anc โŠข ( ๐‘‡ โˆˆ BndLinOp โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
14 lnopcon โŠข ( ๐‘‡ โˆˆ LinOp โ†’ ( ๐‘‡ โˆˆ ContOp โ†” โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โ‰ค ( ๐‘ฅ ยท ( normโ„Ž โ€˜ ๐‘ฆ ) ) ) )
15 13 14 imbitrrid โŠข ( ๐‘‡ โˆˆ LinOp โ†’ ( ๐‘‡ โˆˆ BndLinOp โ†’ ๐‘‡ โˆˆ ContOp ) )
16 5 15 impbid โŠข ( ๐‘‡ โˆˆ LinOp โ†’ ( ๐‘‡ โˆˆ ContOp โ†” ๐‘‡ โˆˆ BndLinOp ) )