unopbd

Description: A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	unopbd	$⊢ T \in UniOp \to T \in BndLinOp$

Step	Hyp	Ref	Expression
1		unoplin	$⊢ T \in UniOp \to T \in LinOp$
2		unopf1o	$⊢ T \in UniOp \to T : ℋ \underset{1-1 onto}{⟶} ℋ$
3		f1of	$⊢ T : ℋ \underset{1-1 onto}{⟶} ℋ \to T : ℋ ⟶ ℋ$
4	2 3	syl	$⊢ T \in UniOp \to T : ℋ ⟶ ℋ$
5		nmop0h	$⊢ (ℋ = 0_{ℋ} \land T : ℋ ⟶ ℋ) \to {norm}_{op} (T) = 0$
6		0re	$⊢ 0 \in ℝ$
7	5 6	eqeltrdi	$⊢ (ℋ = 0_{ℋ} \land T : ℋ ⟶ ℋ) \to {norm}_{op} (T) \in ℝ$
8	4 7	sylan2	$⊢ (ℋ = 0_{ℋ} \land T \in UniOp) \to {norm}_{op} (T) \in ℝ$
9		df-ne	$⊢ ℋ \neq 0_{ℋ} \leftrightarrow \neg ℋ = 0_{ℋ}$
10		nmopun	$⊢ (ℋ \neq 0_{ℋ} \land T \in UniOp) \to {norm}_{op} (T) = 1$
11		1re	$⊢ 1 \in ℝ$
12	10 11	eqeltrdi	$⊢ (ℋ \neq 0_{ℋ} \land T \in UniOp) \to {norm}_{op} (T) \in ℝ$
13	9 12	sylanbr	$⊢ (\neg ℋ = 0_{ℋ} \land T \in UniOp) \to {norm}_{op} (T) \in ℝ$
14	8 13	pm2.61ian	$⊢ T \in UniOp \to {norm}_{op} (T) \in ℝ$
15		elbdop2	$⊢ T \in BndLinOp \leftrightarrow (T \in LinOp \land {norm}_{op} (T) \in ℝ)$
16	1 14 15	sylanbrc	$⊢ T \in UniOp \to T \in BndLinOp$

Metamath Proof Explorer