Metamath Proof Explorer

Theorem lnfncnbd

Description: A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nmcfnex	$⊢ (T \in LinFn \land T \in ContFn) \to {norm}_{fn} (T) \in ℝ$
2	1	ex	$⊢ T \in LinFn \to (T \in ContFn \to {norm}_{fn} (T) \in ℝ)$
3		simpr	$⊢ (T \in LinFn \land {norm}_{fn} (T) \in ℝ) \to {norm}_{fn} (T) \in ℝ$
4		nmbdfnlb	$⊢ (T \in LinFn \land {norm}_{fn} (T) \in ℝ \land y \in ℋ) \to \|T (y)\| \leq {norm}_{fn} (T) {norm}_{ℎ} (y)$
5	4	3expa	$⊢ ((T \in LinFn \land {norm}_{fn} (T) \in ℝ) \land y \in ℋ) \to \|T (y)\| \leq {norm}_{fn} (T) {norm}_{ℎ} (y)$
6	5	ralrimiva	$⊢ (T \in LinFn \land {norm}_{fn} (T) \in ℝ) \to \forall y \in ℋ \|T (y)\| \leq {norm}_{fn} (T) {norm}_{ℎ} (y)$
7		oveq1	$⊢ x = {norm}_{fn} (T) \to x {norm}_{ℎ} (y) = {norm}_{fn} (T) {norm}_{ℎ} (y)$
8	7	breq2d	$⊢ x = {norm}_{fn} (T) \to (\|T (y)\| \leq x {norm}_{ℎ} (y) \leftrightarrow \|T (y)\| \leq {norm}_{fn} (T) {norm}_{ℎ} (y))$
9	8	ralbidv	$⊢ x = {norm}_{fn} (T) \to (\forall y \in ℋ \|T (y)\| \leq x {norm}_{ℎ} (y) \leftrightarrow \forall y \in ℋ \|T (y)\| \leq {norm}_{fn} (T) {norm}_{ℎ} (y))$
10	9	rspcev	$⊢ ({norm}_{fn} (T) \in ℝ \land \forall y \in ℋ \|T (y)\| \leq {norm}_{fn} (T) {norm}_{ℎ} (y)) \to \exists x \in ℝ \forall y \in ℋ \|T (y)\| \leq x {norm}_{ℎ} (y)$
11	3 6 10	syl2anc	$⊢ (T \in LinFn \land {norm}_{fn} (T) \in ℝ) \to \exists x \in ℝ \forall y \in ℋ \|T (y)\| \leq x {norm}_{ℎ} (y)$
12	11	ex	$⊢ T \in LinFn \to ({norm}_{fn} (T) \in ℝ \to \exists x \in ℝ \forall y \in ℋ \|T (y)\| \leq x {norm}_{ℎ} (y))$
13		lnfncon	$⊢ T \in LinFn \to (T \in ContFn \leftrightarrow \exists x \in ℝ \forall y \in ℋ \|T (y)\| \leq x {norm}_{ℎ} (y))$
14	12 13	sylibrd	$⊢ T \in LinFn \to ({norm}_{fn} (T) \in ℝ \to T \in ContFn)$
15	2 14	impbid	$⊢ T \in LinFn \to (T \in ContFn \leftrightarrow {norm}_{fn} (T) \in ℝ)$