This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- T e. BndLinOp
Assertion bdophmi 
|- ( A e. CC -> ( A .op T ) e. BndLinOp )

Proof

Step Hyp Ref Expression
1 nmophm.1 
 |-  T e. BndLinOp
2 bdopln 
 |-  ( T e. BndLinOp -> T e. LinOp )
3 1 2 ax-mp 
 |-  T e. LinOp
4 3 lnopmi 
 |-  ( A e. CC -> ( A .op T ) e. LinOp )
5 1 nmophmi 
 |-  ( A e. CC -> ( normop ` ( A .op T ) ) = ( ( abs ` A ) x. ( normop ` T ) ) )
6 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
7 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
8 1 7 ax-mp 
 |-  ( normop ` T ) e. RR
9 remulcl 
 |-  ( ( ( abs ` A ) e. RR /\ ( normop ` T ) e. RR ) -> ( ( abs ` A ) x. ( normop ` T ) ) e. RR )
10 6 8 9 sylancl 
 |-  ( A e. CC -> ( ( abs ` A ) x. ( normop ` T ) ) e. RR )
11 5 10 eqeltrd 
 |-  ( A e. CC -> ( normop ` ( A .op T ) ) e. RR )
12 elbdop2 
 |-  ( ( A .op T ) e. BndLinOp <-> ( ( A .op T ) e. LinOp /\ ( normop ` ( A .op T ) ) e. RR ) )
13 4 11 12 sylanbrc 
 |-  ( A e. CC -> ( A .op T ) e. BndLinOp )