psercn

Description: An infinite series converges to a continuous function on the open disk of radius R , where R is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015)

	Ref	Expression
Hypotheses	pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
	pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
	psercn.s	$⊢ S = {abs}^{-1} [[0, R)]$
	psercn.m	$⊢ M = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
Assertion	psercn	$⊢ φ \to F : S \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
3		pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
4		pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
5		psercn.s	$⊢ S = {abs}^{-1} [[0, R)]$
6		psercn.m	$⊢ M = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
7		sumex	$⊢ \sum_{j \in ℕ_{0}} G (y) (j) \in V$
8	7	rgenw	$⊢ \forall y \in S \sum_{j \in ℕ_{0}} G (y) (j) \in V$
9	2	fnmpt	$⊢ \forall y \in S \sum_{j \in ℕ_{0}} G (y) (j) \in V \to F Fn S$
10	8 9	mp1i	$⊢ φ \to F Fn S$
11		cnvimass	$⊢ {abs}^{-1} [[0, R)] \subseteq dom abs$
12		absf	$⊢ abs : ℂ ⟶ ℝ$
13	12	fdmi	$⊢ dom abs = ℂ$
14	11 13	sseqtri	$⊢ {abs}^{-1} [[0, R)] \subseteq ℂ$
15	5 14	eqsstri	$⊢ S \subseteq ℂ$
16	15	a1i	$⊢ φ \to S \subseteq ℂ$
17	16	sselda	$⊢ (φ \land a \in S) \to a \in ℂ$
18		0cn	$⊢ 0 \in ℂ$
19		eqid	$⊢ abs \circ - = abs \circ -$
20	19	cnmetdval	$⊢ (0 \in ℂ \land a \in ℂ) \to 0 (abs \circ -) a = \|0 - a\|$
21	18 17 20	sylancr	$⊢ (φ \land a \in S) \to 0 (abs \circ -) a = \|0 - a\|$
22		abssub	$⊢ (0 \in ℂ \land a \in ℂ) \to \|0 - a\| = \|a - 0\|$
23	18 17 22	sylancr	$⊢ (φ \land a \in S) \to \|0 - a\| = \|a - 0\|$
24	17	subid1d	$⊢ (φ \land a \in S) \to a - 0 = a$
25	24	fveq2d	$⊢ (φ \land a \in S) \to \|a - 0\| = \|a\|$
26	21 23 25	3eqtrd	$⊢ (φ \land a \in S) \to 0 (abs \circ -) a = \|a\|$
27		breq2	$⊢ \frac{\|a\| + R}{2} = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) \to (\|a\| < \frac{\|a\| + R}{2} \leftrightarrow \|a\| < if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1))$
28		breq2	$⊢ \|a\| + 1 = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) \to (\|a\| < \|a\| + 1 \leftrightarrow \|a\| < if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1))$
29		simpr	$⊢ (φ \land a \in S) \to a \in S$
30	29 5	eleqtrdi	$⊢ (φ \land a \in S) \to a \in {abs}^{-1} [[0, R)]$
31		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
32		elpreima	$⊢ abs Fn ℂ \to (a \in {abs}^{-1} [[0, R)] \leftrightarrow (a \in ℂ \land \|a\| \in [0, R)))$
33	12 31 32	mp2b	$⊢ a \in {abs}^{-1} [[0, R)] \leftrightarrow (a \in ℂ \land \|a\| \in [0, R))$
34	30 33	sylib	$⊢ (φ \land a \in S) \to (a \in ℂ \land \|a\| \in [0, R))$
35	34	simprd	$⊢ (φ \land a \in S) \to \|a\| \in [0, R)$
36		0re	$⊢ 0 \in ℝ$
37		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
38	1 3 4	radcnvcl	$⊢ φ \to R \in [0, +∞]$
39	38	adantr	$⊢ (φ \land a \in S) \to R \in [0, +∞]$
40	37 39	sselid	$⊢ (φ \land a \in S) \to R \in ℝ^{*}$
41		elico2	$⊢ (0 \in ℝ \land R \in ℝ^{*}) \to (\|a\| \in [0, R) \leftrightarrow (\|a\| \in ℝ \land 0 \leq \|a\| \land \|a\| < R))$
42	36 40 41	sylancr	$⊢ (φ \land a \in S) \to (\|a\| \in [0, R) \leftrightarrow (\|a\| \in ℝ \land 0 \leq \|a\| \land \|a\| < R))$
43	35 42	mpbid	$⊢ (φ \land a \in S) \to (\|a\| \in ℝ \land 0 \leq \|a\| \land \|a\| < R)$
44	43	simp3d	$⊢ (φ \land a \in S) \to \|a\| < R$
45	44	adantr	$⊢ ((φ \land a \in S) \land R \in ℝ) \to \|a\| < R$
46	17	abscld	$⊢ (φ \land a \in S) \to \|a\| \in ℝ$
47		avglt1	$⊢ (\|a\| \in ℝ \land R \in ℝ) \to (\|a\| < R \leftrightarrow \|a\| < \frac{\|a\| + R}{2})$
48	46 47	sylan	$⊢ ((φ \land a \in S) \land R \in ℝ) \to (\|a\| < R \leftrightarrow \|a\| < \frac{\|a\| + R}{2})$
49	45 48	mpbid	$⊢ ((φ \land a \in S) \land R \in ℝ) \to \|a\| < \frac{\|a\| + R}{2}$
50	46	ltp1d	$⊢ (φ \land a \in S) \to \|a\| < \|a\| + 1$
51	50	adantr	$⊢ ((φ \land a \in S) \land \neg R \in ℝ) \to \|a\| < \|a\| + 1$
52	27 28 49 51	ifbothda	$⊢ (φ \land a \in S) \to \|a\| < if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
53	52 6	breqtrrdi	$⊢ (φ \land a \in S) \to \|a\| < M$
54	26 53	eqbrtrd	$⊢ (φ \land a \in S) \to 0 (abs \circ -) a < M$
55		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
56	1 2 3 4 5 6	psercnlem1	$⊢ (φ \land a \in S) \to (M \in ℝ^{+} \land \|a\| < M \land M < R)$
57	56	simp1d	$⊢ (φ \land a \in S) \to M \in ℝ^{+}$
58	57	rpxrd	$⊢ (φ \land a \in S) \to M \in ℝ^{*}$
59		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land M \in ℝ^{*}) \to (a \in (0 ball (abs \circ -) M) \leftrightarrow (a \in ℂ \land 0 (abs \circ -) a < M))$
60	55 18 58 59	mp3an12i	$⊢ (φ \land a \in S) \to (a \in (0 ball (abs \circ -) M) \leftrightarrow (a \in ℂ \land 0 (abs \circ -) a < M))$
61	17 54 60	mpbir2and	$⊢ (φ \land a \in S) \to a \in (0 ball (abs \circ -) M)$
62	61	fvresd	$⊢ (φ \land a \in S) \to ({F ↾}_{(0 ball (abs \circ -) M)}) (a) = F (a)$
63	2	reseq1i	$⊢ {F ↾}_{(0 ball (abs \circ -) M)} = {(y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j)) ↾}_{(0 ball (abs \circ -) M)}$
64	1 2 3 4 5 56	psercnlem2	$⊢ (φ \land a \in S) \to (a \in (0 ball (abs \circ -) M) \land 0 ball (abs \circ -) M \subseteq {abs}^{-1} [[0, M]] \land {abs}^{-1} [[0, M]] \subseteq S)$
65	64	simp2d	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) M \subseteq {abs}^{-1} [[0, M]]$
66	64	simp3d	$⊢ (φ \land a \in S) \to {abs}^{-1} [[0, M]] \subseteq S$
67	65 66	sstrd	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) M \subseteq S$
68	67	resmptd	$⊢ (φ \land a \in S) \to {(y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j)) ↾}_{(0 ball (abs \circ -) M)} = (y \in (0 ball (abs \circ -) M) ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
69	63 68	eqtrid	$⊢ (φ \land a \in S) \to {F ↾}_{(0 ball (abs \circ -) M)} = (y \in (0 ball (abs \circ -) M) ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
70		eqid	$⊢ (y \in (0 ball (abs \circ -) M) ⟼ \sum_{j \in ℕ_{0}} G (y) (j)) = (y \in (0 ball (abs \circ -) M) ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
71	3	adantr	$⊢ (φ \land a \in S) \to A : ℕ_{0} ⟶ ℂ$
72		fveq2	$⊢ k = y \to G (k) = G (y)$
73	72	seqeq3d	$⊢ k = y \to seq 0 (+ G (k)) = seq 0 (+ G (y))$
74	73	fveq1d	$⊢ k = y \to seq 0 (+ G (k)) (s) = seq 0 (+ G (y)) (s)$
75	74	cbvmptv	$⊢ (k \in (0 ball (abs \circ -) M) ⟼ seq 0 (+ G (k)) (s)) = (y \in (0 ball (abs \circ -) M) ⟼ seq 0 (+ G (y)) (s))$
76		fveq2	$⊢ s = i \to seq 0 (+ G (y)) (s) = seq 0 (+ G (y)) (i)$
77	76	mpteq2dv	$⊢ s = i \to (y \in (0 ball (abs \circ -) M) ⟼ seq 0 (+ G (y)) (s)) = (y \in (0 ball (abs \circ -) M) ⟼ seq 0 (+ G (y)) (i))$
78	75 77	eqtrid	$⊢ s = i \to (k \in (0 ball (abs \circ -) M) ⟼ seq 0 (+ G (k)) (s)) = (y \in (0 ball (abs \circ -) M) ⟼ seq 0 (+ G (y)) (i))$
79	78	cbvmptv	$⊢ (s \in ℕ_{0} ⟼ (k \in (0 ball (abs \circ -) M) ⟼ seq 0 (+ G (k)) (s))) = (i \in ℕ_{0} ⟼ (y \in (0 ball (abs \circ -) M) ⟼ seq 0 (+ G (y)) (i)))$
80	57	rpred	$⊢ (φ \land a \in S) \to M \in ℝ$
81	56	simp3d	$⊢ (φ \land a \in S) \to M < R$
82	1 70 71 4 79 80 81 65	psercn2	$⊢ (φ \land a \in S) \to (y \in (0 ball (abs \circ -) M) ⟼ \sum_{j \in ℕ_{0}} G (y) (j)) : (0 ball (abs \circ -) M) \underset{cn}{⟶} ℂ$
83	69 82	eqeltrd	$⊢ (φ \land a \in S) \to ({F ↾}_{(0 ball (abs \circ -) M)}) : (0 ball (abs \circ -) M) \underset{cn}{⟶} ℂ$
84		cncff	$⊢ ({F ↾}_{(0 ball (abs \circ -) M)}) : (0 ball (abs \circ -) M) \underset{cn}{⟶} ℂ \to ({F ↾}_{(0 ball (abs \circ -) M)}) : 0 ball (abs \circ -) M ⟶ ℂ$
85	83 84	syl	$⊢ (φ \land a \in S) \to ({F ↾}_{(0 ball (abs \circ -) M)}) : 0 ball (abs \circ -) M ⟶ ℂ$
86	85 61	ffvelrnd	$⊢ (φ \land a \in S) \to ({F ↾}_{(0 ball (abs \circ -) M)}) (a) \in ℂ$
87	62 86	eqeltrrd	$⊢ (φ \land a \in S) \to F (a) \in ℂ$
88	87	ralrimiva	$⊢ φ \to \forall a \in S F (a) \in ℂ$
89		ffnfv	$⊢ F : S ⟶ ℂ \leftrightarrow (F Fn S \land \forall a \in S F (a) \in ℂ)$
90	10 88 89	sylanbrc	$⊢ φ \to F : S ⟶ ℂ$
91	67 15	sstrdi	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) M \subseteq ℂ$
92		ssid	$⊢ ℂ \subseteq ℂ$
93		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
94		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M) = TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)$
95	93	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
96	95	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
97	93 94 96	cncfcn	$⊢ (0 ball (abs \circ -) M \subseteq ℂ \land ℂ \subseteq ℂ) \to (0 ball (abs \circ -) M) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) Cn TopOpen (ℂ_{fld})$
98	91 92 97	sylancl	$⊢ (φ \land a \in S) \to (0 ball (abs \circ -) M) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) Cn TopOpen (ℂ_{fld})$
99	83 98	eleqtrd	$⊢ (φ \land a \in S) \to {F ↾}_{(0 ball (abs \circ -) M)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) Cn TopOpen (ℂ_{fld}))$
100	93	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
101		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
102	101	restuni	$⊢ (TopOpen (ℂ_{fld}) \in Top \land 0 ball (abs \circ -) M \subseteq ℂ) \to 0 ball (abs \circ -) M = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M))$
103	100 91 102	sylancr	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) M = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M))$
104	61 103	eleqtrd	$⊢ (φ \land a \in S) \to a \in ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M))$
105		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M))$
106	105	cncnpi	$⊢ ({F ↾}_{(0 ball (abs \circ -) M)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) Cn TopOpen (ℂ_{fld})) \land a \in ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M))) \to {F ↾}_{(0 ball (abs \circ -) M)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld})) (a)$
107	99 104 106	syl2anc	$⊢ (φ \land a \in S) \to {F ↾}_{(0 ball (abs \circ -) M)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld})) (a)$
108		cnex	$⊢ ℂ \in V$
109	108 15	ssexi	$⊢ S \in V$
110	109	a1i	$⊢ (φ \land a \in S) \to S \in V$
111		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land 0 ball (abs \circ -) M \subseteq S \land S \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} S) ↾_{𝑡} (0 ball (abs \circ -) M) = TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)$
112	100 67 110 111	mp3an2i	$⊢ (φ \land a \in S) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} S) ↾_{𝑡} (0 ball (abs \circ -) M) = TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)$
113	112	oveq1d	$⊢ (φ \land a \in S) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld}) = (TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld})$
114	113	fveq1d	$⊢ (φ \land a \in S) \to (((TopOpen (ℂ_{fld}) ↾_{𝑡} S) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld})) (a) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld})) (a)$
115	107 114	eleqtrrd	$⊢ (φ \land a \in S) \to {F ↾}_{(0 ball (abs \circ -) M)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} S) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld})) (a)$
116		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land S \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
117	100 109 116	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
118	117	a1i	$⊢ (φ \land a \in S) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
119		df-ss	$⊢ 0 ball (abs \circ -) M \subseteq S \leftrightarrow (0 ball (abs \circ -) M) \cap S = 0 ball (abs \circ -) M$
120	67 119	sylib	$⊢ (φ \land a \in S) \to (0 ball (abs \circ -) M) \cap S = 0 ball (abs \circ -) M$
121	93	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
122	121	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land M \in ℝ^{*}) \to 0 ball (abs \circ -) M \in TopOpen (ℂ_{fld})$
123	55 18 58 122	mp3an12i	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) M \in TopOpen (ℂ_{fld})$
124		elrestr	$⊢ (TopOpen (ℂ_{fld}) \in Top \land S \in V \land 0 ball (abs \circ -) M \in TopOpen (ℂ_{fld})) \to (0 ball (abs \circ -) M) \cap S \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
125	100 109 123 124	mp3an12i	$⊢ (φ \land a \in S) \to (0 ball (abs \circ -) M) \cap S \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
126	120 125	eqeltrrd	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) M \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
127		isopn3i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top \land 0 ball (abs \circ -) M \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (0 ball (abs \circ -) M) = 0 ball (abs \circ -) M$
128	117 126 127	sylancr	$⊢ (φ \land a \in S) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (0 ball (abs \circ -) M) = 0 ball (abs \circ -) M$
129	61 128	eleqtrrd	$⊢ (φ \land a \in S) \to a \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (0 ball (abs \circ -) M)$
130	90	adantr	$⊢ (φ \land a \in S) \to F : S ⟶ ℂ$
131	101	restuni	$⊢ (TopOpen (ℂ_{fld}) \in Top \land S \subseteq ℂ) \to S = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
132	100 15 131	mp2an	$⊢ S = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
133	132 101	cnprest	$⊢ ((TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top \land 0 ball (abs \circ -) M \subseteq S) \land (a \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (0 ball (abs \circ -) M) \land F : S ⟶ ℂ)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) CnP TopOpen (ℂ_{fld})) (a) \leftrightarrow {F ↾}_{(0 ball (abs \circ -) M)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} S) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld})) (a))$
134	118 67 129 130 133	syl22anc	$⊢ (φ \land a \in S) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) CnP TopOpen (ℂ_{fld})) (a) \leftrightarrow {F ↾}_{(0 ball (abs \circ -) M)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} S) ↾_{𝑡} (0 ball (abs \circ -) M)) CnP TopOpen (ℂ_{fld})) (a))$
135	115 134	mpbird	$⊢ (φ \land a \in S) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) CnP TopOpen (ℂ_{fld})) (a)$
136	135	ralrimiva	$⊢ φ \to \forall a \in S F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) CnP TopOpen (ℂ_{fld})) (a)$
137		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land S \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
138	95 15 137	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
139		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn TopOpen (ℂ_{fld})) \leftrightarrow (F : S ⟶ ℂ \land \forall a \in S F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) CnP TopOpen (ℂ_{fld})) (a)))$
140	138 95 139	mp2an	$⊢ F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn TopOpen (ℂ_{fld})) \leftrightarrow (F : S ⟶ ℂ \land \forall a \in S F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) CnP TopOpen (ℂ_{fld})) (a))$
141	90 136 140	sylanbrc	$⊢ φ \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn TopOpen (ℂ_{fld}))$
142		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
143	93 142 96	cncfcn	$⊢ (S \subseteq ℂ \land ℂ \subseteq ℂ) \to S \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn TopOpen (ℂ_{fld})$
144	15 92 143	mp2an	$⊢ S \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn TopOpen (ℂ_{fld})$
145	141 144	eleqtrrdi	$⊢ φ \to F : S \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem psercn

Proof