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 )