Metamath Proof Explorer

Theorem nmcopex

Description: The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	nmcopex	$⊢ (T \in LinOp \land T \in ContOp) \to {norm}_{op} (T) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ T \in (LinOp \cap ContOp) \leftrightarrow (T \in LinOp \land T \in ContOp)$
2		fveq2	$⊢ T = if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \to {norm}_{op} (T) = {norm}_{op} (if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}))$
3	2	eleq1d	$⊢ T = if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \to ({norm}_{op} (T) \in ℝ \leftrightarrow {norm}_{op} (if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ})) \in ℝ)$
4		idlnop	$⊢ {I ↾}_{ℋ} \in LinOp$
5		idcnop	$⊢ {I ↾}_{ℋ} \in ContOp$
6		elin	$⊢ {I ↾}_{ℋ} \in (LinOp \cap ContOp) \leftrightarrow ({I ↾}_{ℋ} \in LinOp \land {I ↾}_{ℋ} \in ContOp)$
7	4 5 6	mpbir2an	$⊢ {I ↾}_{ℋ} \in (LinOp \cap ContOp)$
8	7	elimel	$⊢ if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \in (LinOp \cap ContOp)$
9		elin	$⊢ if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \in (LinOp \cap ContOp) \leftrightarrow (if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \in LinOp \land if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \in ContOp)$
10	8 9	mpbi	$⊢ (if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \in LinOp \land if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \in ContOp)$
11	10	simpli	$⊢ if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \in LinOp$
12	10	simpri	$⊢ if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ}) \in ContOp$
13	11 12	nmcopexi	$⊢ {norm}_{op} (if (T \in (LinOp \cap ContOp), T, {I ↾}_{ℋ})) \in ℝ$
14	3 13	dedth	$⊢ T \in (LinOp \cap ContOp) \to {norm}_{op} (T) \in ℝ$
15	1 14	sylbir	$⊢ (T \in LinOp \land T \in ContOp) \to {norm}_{op} (T) \in ℝ$