Metamath Proof Explorer

Theorem nmcfnex

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

		Ref	Expression
	Assertion	nmcfnex	$⊢ (T \in LinFn \land T \in ContFn) \to {norm}_{fn} (T) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ T \in (LinFn \cap ContFn) \leftrightarrow (T \in LinFn \land T \in ContFn)$
2		fveq2	$⊢ T = if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \to {norm}_{fn} (T) = {norm}_{fn} (if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}))$
3	2	eleq1d	$⊢ T = if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \to ({norm}_{fn} (T) \in ℝ \leftrightarrow {norm}_{fn} (if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\})) \in ℝ)$
4		0lnfn	$⊢ ℋ \times \{0\} \in LinFn$
5		0cnfn	$⊢ ℋ \times \{0\} \in ContFn$
6		elin	$⊢ ℋ \times \{0\} \in (LinFn \cap ContFn) \leftrightarrow (ℋ \times \{0\} \in LinFn \land ℋ \times \{0\} \in ContFn)$
7	4 5 6	mpbir2an	$⊢ ℋ \times \{0\} \in (LinFn \cap ContFn)$
8	7	elimel	$⊢ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in (LinFn \cap ContFn)$
9		elin	$⊢ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in (LinFn \cap ContFn) \leftrightarrow (if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in LinFn \land if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in ContFn)$
10	8 9	mpbi	$⊢ (if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in LinFn \land if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in ContFn)$
11	10	simpli	$⊢ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in LinFn$
12	10	simpri	$⊢ if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\}) \in ContFn$
13	11 12	nmcfnexi	$⊢ {norm}_{fn} (if (T \in (LinFn \cap ContFn), T, ℋ \times \{0\})) \in ℝ$
14	3 13	dedth	$⊢ T \in (LinFn \cap ContFn) \to {norm}_{fn} (T) \in ℝ$
15	1 14	sylbir	$⊢ (T \in LinFn \land T \in ContFn) \to {norm}_{fn} (T) \in ℝ$