nmcvcn

Description: The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007) (Proof shortened by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmcvcn.1	$⊢ N = {norm}_{CV} (U)$
	nmcvcn.2	$⊢ C = IndMet (U)$
	nmcvcn.j	$⊢ J = MetOpen (C)$
	nmcvcn.k	$⊢ K = topGen (ran (.))$
Assertion	nmcvcn	$⊢ U \in NrmCVec \to N \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		nmcvcn.1	$⊢ N = {norm}_{CV} (U)$
2		nmcvcn.2	$⊢ C = IndMet (U)$
3		nmcvcn.j	$⊢ J = MetOpen (C)$
4		nmcvcn.k	$⊢ K = topGen (ran (.))$
5		eqid	$⊢ BaseSet (U) = BaseSet (U)$
6	5 1	nvf	$⊢ U \in NrmCVec \to N : BaseSet (U) ⟶ ℝ$
7		simprr	$⊢ (U \in NrmCVec \land (x \in BaseSet (U) \land e \in ℝ^{+})) \to e \in ℝ^{+}$
8	5 1	nvcl	$⊢ (U \in NrmCVec \land x \in BaseSet (U)) \to N (x) \in ℝ$
9	8	ex	$⊢ U \in NrmCVec \to (x \in BaseSet (U) \to N (x) \in ℝ)$
10	5 1	nvcl	$⊢ (U \in NrmCVec \land y \in BaseSet (U)) \to N (y) \in ℝ$
11	10	ex	$⊢ U \in NrmCVec \to (y \in BaseSet (U) \to N (y) \in ℝ)$
12	9 11	anim12d	$⊢ U \in NrmCVec \to ((x \in BaseSet (U) \land y \in BaseSet (U)) \to (N (x) \in ℝ \land N (y) \in ℝ))$
13		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
14	13	remet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in Met (ℝ)$
15		metcl	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in Met (ℝ) \land N (x) \in ℝ \land N (y) \in ℝ) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ$
16	14 15	mp3an1	$⊢ (N (x) \in ℝ \land N (y) \in ℝ) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ$
17	12 16	syl6	$⊢ U \in NrmCVec \to ((x \in BaseSet (U) \land y \in BaseSet (U)) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ)$
18	17	3impib	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ$
19	5 2	imsmet	$⊢ U \in NrmCVec \to C \in Met (BaseSet (U))$
20		metcl	$⊢ (C \in Met (BaseSet (U)) \land x \in BaseSet (U) \land y \in BaseSet (U)) \to x C y \in ℝ$
21	19 20	syl3an1	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to x C y \in ℝ$
22		eqid	$⊢ +_{v} (U) = +_{v} (U)$
23		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
24	5 22 23 1	nvabs	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to \|N (x) - N (y)\| \leq N (x +_{v} (U) (-1 \cdot_{𝑠OLD} (U) y))$
25	12	3impib	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to (N (x) \in ℝ \land N (y) \in ℝ)$
26	13	remetdval	$⊢ (N (x) \in ℝ \land N (y) \in ℝ) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) = \|N (x) - N (y)\|$
27	25 26	syl	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) = \|N (x) - N (y)\|$
28	5 22 23 1 2	imsdval2	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to x C y = N (x +_{v} (U) (-1 \cdot_{𝑠OLD} (U) y))$
29	24 27 28	3brtr4d	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \leq x C y$
30	18 21 29	jca31	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to ((N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ \land x C y \in ℝ) \land N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \leq x C y)$
31	30	3expa	$⊢ ((U \in NrmCVec \land x \in BaseSet (U)) \land y \in BaseSet (U)) \to ((N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ \land x C y \in ℝ) \land N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \leq x C y)$
32		rpre	$⊢ e \in ℝ^{+} \to e \in ℝ$
33		lelttr	$⊢ (N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ \land x C y \in ℝ \land e \in ℝ) \to ((N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \leq x C y \land x C y < e) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
34	33	3expa	$⊢ ((N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ \land x C y \in ℝ) \land e \in ℝ) \to ((N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \leq x C y \land x C y < e) \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
35	34	expdimp	$⊢ (((N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ \land x C y \in ℝ) \land e \in ℝ) \land N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \leq x C y) \to (x C y < e \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
36	35	an32s	$⊢ (((N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \in ℝ \land x C y \in ℝ) \land N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) \leq x C y) \land e \in ℝ) \to (x C y < e \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
37	31 32 36	syl2an	$⊢ (((U \in NrmCVec \land x \in BaseSet (U)) \land y \in BaseSet (U)) \land e \in ℝ^{+}) \to (x C y < e \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
38	37	ex	$⊢ ((U \in NrmCVec \land x \in BaseSet (U)) \land y \in BaseSet (U)) \to (e \in ℝ^{+} \to (x C y < e \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e))$
39	38	ralrimdva	$⊢ (U \in NrmCVec \land x \in BaseSet (U)) \to (e \in ℝ^{+} \to \forall y \in BaseSet (U) (x C y < e \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e))$
40	39	impr	$⊢ (U \in NrmCVec \land (x \in BaseSet (U) \land e \in ℝ^{+})) \to \forall y \in BaseSet (U) (x C y < e \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
41		breq2	$⊢ d = e \to (x C y < d \leftrightarrow x C y < e)$
42	41	rspceaimv	$⊢ (e \in ℝ^{+} \land \forall y \in BaseSet (U) (x C y < e \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)) \to \exists d \in ℝ^{+} \forall y \in BaseSet (U) (x C y < d \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
43	7 40 42	syl2anc	$⊢ (U \in NrmCVec \land (x \in BaseSet (U) \land e \in ℝ^{+})) \to \exists d \in ℝ^{+} \forall y \in BaseSet (U) (x C y < d \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
44	43	ralrimivva	$⊢ U \in NrmCVec \to \forall x \in BaseSet (U) \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in BaseSet (U) (x C y < d \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)$
45	5 2	imsxmet	$⊢ U \in NrmCVec \to C \in ∞Met (BaseSet (U))$
46	13	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
47		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
48	13 47	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
49	4 48	eqtri	$⊢ K = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
50	3 49	metcn	$⊢ (C \in ∞Met (BaseSet (U)) \land {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)) \to (N \in (J Cn K) \leftrightarrow (N : BaseSet (U) ⟶ ℝ \land \forall x \in BaseSet (U) \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in BaseSet (U) (x C y < d \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)))$
51	45 46 50	sylancl	$⊢ U \in NrmCVec \to (N \in (J Cn K) \leftrightarrow (N : BaseSet (U) ⟶ ℝ \land \forall x \in BaseSet (U) \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in BaseSet (U) (x C y < d \to N (x) ({(abs \circ -) ↾}_{ℝ^{2}}) N (y) < e)))$
52	6 44 51	mpbir2and	$⊢ U \in NrmCVec \to N \in (J Cn K)$

Metamath Proof Explorer

Theorem nmcvcn

Proof