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

Proof

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