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 ⊢ 𝑇 ∈ 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 )