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\in \mathrm{BndLinOp}$$
Assertion	bdophmi	$$⊢A\in ℂ\to A{·}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$

Proof

Step	Hyp	Ref	Expression
1		nmophm.1	$$⊢T\in \mathrm{BndLinOp}$$
2		bdopln	$$⊢T\in \mathrm{BndLinOp}\to T\in \mathrm{LinOp}$$
3	1 2	ax-mp	$$⊢T\in \mathrm{LinOp}$$
4	3	lnopmi	$$⊢A\in ℂ\to A{·}_{\mathrm{op}}T\in \mathrm{LinOp}$$
5	1	nmophmi	$$⊢A\in ℂ\to {norm}_{\mathrm{op}}\left(A{·}_{\mathrm{op}}T\right)=\left|A\right|{norm}_{\mathrm{op}}\left(T\right)$$
6		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
7		nmopre	$$⊢T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
8	1 7	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
9		remulcl	$$⊢\left(\left|A\right|\in ℝ\wedge {norm}_{\mathrm{op}}\left(T\right)\in ℝ\right)\to \left|A\right|{norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
10	6 8 9	sylancl	$$⊢A\in ℂ\to \left|A\right|{norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
11	5 10	eqeltrd	$$⊢A\in ℂ\to {norm}_{\mathrm{op}}\left(A{·}_{\mathrm{op}}T\right)\in ℝ$$
12		elbdop2	$$⊢A{·}_{\mathrm{op}}T\in \mathrm{BndLinOp}\leftrightarrow \left(A{·}_{\mathrm{op}}T\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left(A{·}_{\mathrm{op}}T\right)\in ℝ\right)$$
13	4 11 12	sylanbrc	$$⊢A\in ℂ\to A{·}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$