# 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}\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}↔\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}$