Metamath Proof Explorer


Theorem bdophmi

Description: The scalar product of a bounded linear operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmophm.1 โŠข ๐‘‡ โˆˆ BndLinOp
Assertion bdophmi ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด ยทop ๐‘‡ ) โˆˆ BndLinOp )

Proof

Step Hyp Ref Expression
1 nmophm.1 โŠข ๐‘‡ โˆˆ BndLinOp
2 bdopln โŠข ( ๐‘‡ โˆˆ BndLinOp โ†’ ๐‘‡ โˆˆ LinOp )
3 1 2 ax-mp โŠข ๐‘‡ โˆˆ LinOp
4 3 lnopmi โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด ยทop ๐‘‡ ) โˆˆ LinOp )
5 1 nmophmi โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( normop โ€˜ ( ๐ด ยทop ๐‘‡ ) ) = ( ( abs โ€˜ ๐ด ) ยท ( normop โ€˜ ๐‘‡ ) ) )
6 abscl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( abs โ€˜ ๐ด ) โˆˆ โ„ )
7 nmopre โŠข ( ๐‘‡ โˆˆ BndLinOp โ†’ ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ )
8 1 7 ax-mp โŠข ( normop โ€˜ ๐‘‡ ) โˆˆ โ„
9 remulcl โŠข ( ( ( abs โ€˜ ๐ด ) โˆˆ โ„ โˆง ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ ) โ†’ ( ( abs โ€˜ ๐ด ) ยท ( normop โ€˜ ๐‘‡ ) ) โˆˆ โ„ )
10 6 8 9 sylancl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( abs โ€˜ ๐ด ) ยท ( normop โ€˜ ๐‘‡ ) ) โˆˆ โ„ )
11 5 10 eqeltrd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( normop โ€˜ ( ๐ด ยทop ๐‘‡ ) ) โˆˆ โ„ )
12 elbdop2 โŠข ( ( ๐ด ยทop ๐‘‡ ) โˆˆ BndLinOp โ†” ( ( ๐ด ยทop ๐‘‡ ) โˆˆ LinOp โˆง ( normop โ€˜ ( ๐ด ยทop ๐‘‡ ) ) โˆˆ โ„ ) )
13 4 11 12 sylanbrc โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด ยทop ๐‘‡ ) โˆˆ BndLinOp )