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 )