refsumcn

Description: A finite sum of continuous real functions, from a common topological space, is continuous. The class expression for B normally contains free variables k and x to index it. See fsumcn for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	refsumcn.1	$⊢ Ⅎ x φ$
	refsumcn.2	$⊢ K = topGen (ran (.))$
	refsumcn.3	$⊢ φ \to J \in TopOn (X)$
	refsumcn.4	$⊢ φ \to A \in Fin$
	refsumcn.5	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)$
Assertion	refsumcn	$⊢ φ \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		refsumcn.1	$⊢ Ⅎ x φ$
2		refsumcn.2	$⊢ K = topGen (ran (.))$
3		refsumcn.3	$⊢ φ \to J \in TopOn (X)$
4		refsumcn.4	$⊢ φ \to A \in Fin$
5		refsumcn.5	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)$
6		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
7	6	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
8	2 7	eqtri	$⊢ K = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
9	8	oveq2i	$⊢ J Cn K = J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
10	5 9	eleqtrdi	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
11	6	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
12	11	a1i	$⊢ (φ \land k \in A) \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
13	3	adantr	$⊢ (φ \land k \in A) \to J \in TopOn (X)$
14		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
15	2 14	eqeltri	$⊢ K \in TopOn (ℝ)$
16	15	a1i	$⊢ (φ \land k \in A) \to K \in TopOn (ℝ)$
17		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (ℝ) \land (x \in X ⟼ B) \in (J Cn K)) \to (x \in X ⟼ B) : X ⟶ ℝ$
18	13 16 5 17	syl3anc	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) : X ⟶ ℝ$
19	18	frnd	$⊢ (φ \land k \in A) \to ran (x \in X ⟼ B) \subseteq ℝ$
20		ax-resscn	$⊢ ℝ \subseteq ℂ$
21	20	a1i	$⊢ (φ \land k \in A) \to ℝ \subseteq ℂ$
22		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (x \in X ⟼ B) \subseteq ℝ \land ℝ \subseteq ℂ) \to ((x \in X ⟼ B) \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in X ⟼ B) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
23	12 19 21 22	syl3anc	$⊢ (φ \land k \in A) \to ((x \in X ⟼ B) \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in X ⟼ B) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
24	10 23	mpbird	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn TopOpen (ℂ_{fld}))$
25	6 3 4 24	fsumcnf	$⊢ φ \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn TopOpen (ℂ_{fld}))$
26	11	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
27	4	adantr	$⊢ (φ \land x \in X) \to A \in Fin$
28		simpll	$⊢ ((φ \land x \in X) \land k \in A) \to φ$
29		simpr	$⊢ ((φ \land x \in X) \land k \in A) \to k \in A$
30	28 29	jca	$⊢ ((φ \land x \in X) \land k \in A) \to (φ \land k \in A)$
31		simplr	$⊢ ((φ \land x \in X) \land k \in A) \to x \in X$
32		eqid	$⊢ (x \in X ⟼ B) = (x \in X ⟼ B)$
33	32	fmpt	$⊢ \forall x \in X B \in ℝ \leftrightarrow (x \in X ⟼ B) : X ⟶ ℝ$
34	18 33	sylibr	$⊢ (φ \land k \in A) \to \forall x \in X B \in ℝ$
35		rsp	$⊢ \forall x \in X B \in ℝ \to (x \in X \to B \in ℝ)$
36	34 35	syl	$⊢ (φ \land k \in A) \to (x \in X \to B \in ℝ)$
37	30 31 36	sylc	$⊢ ((φ \land x \in X) \land k \in A) \to B \in ℝ$
38	27 37	fsumrecl	$⊢ (φ \land x \in X) \to \sum_{k \in A} B \in ℝ$
39	38	ex	$⊢ φ \to (x \in X \to \sum_{k \in A} B \in ℝ)$
40	1 39	ralrimi	$⊢ φ \to \forall x \in X \sum_{k \in A} B \in ℝ$
41		eqid	$⊢ (x \in X ⟼ \sum_{k \in A} B) = (x \in X ⟼ \sum_{k \in A} B)$
42	41	fnmpt	$⊢ \forall x \in X \sum_{k \in A} B \in ℝ \to (x \in X ⟼ \sum_{k \in A} B) Fn X$
43	40 42	syl	$⊢ φ \to (x \in X ⟼ \sum_{k \in A} B) Fn X$
44		nfcv	$⊢ \underline{Ⅎ} x X$
45		nfcv	$⊢ \underline{Ⅎ} x y$
46		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ \sum_{k \in A} B)$
47	44 45 46	fvelrnbf	$⊢ (x \in X ⟼ \sum_{k \in A} B) Fn X \to (y \in ran (x \in X ⟼ \sum_{k \in A} B) \leftrightarrow \exists x \in X (x \in X ⟼ \sum_{k \in A} B) (x) = y)$
48	43 47	syl	$⊢ φ \to (y \in ran (x \in X ⟼ \sum_{k \in A} B) \leftrightarrow \exists x \in X (x \in X ⟼ \sum_{k \in A} B) (x) = y)$
49	48	biimpa	$⊢ (φ \land y \in ran (x \in X ⟼ \sum_{k \in A} B)) \to \exists x \in X (x \in X ⟼ \sum_{k \in A} B) (x) = y$
50	46	nfrn	$⊢ \underline{Ⅎ} x ran (x \in X ⟼ \sum_{k \in A} B)$
51	50	nfcri	$⊢ Ⅎ x y \in ran (x \in X ⟼ \sum_{k \in A} B)$
52	1 51	nfan	$⊢ Ⅎ x (φ \land y \in ran (x \in X ⟼ \sum_{k \in A} B))$
53		nfcv	$⊢ \underline{Ⅎ} x ℝ$
54	53	nfcri	$⊢ Ⅎ x y \in ℝ$
55		simpr	$⊢ (φ \land x \in X) \to x \in X$
56	55 38	jca	$⊢ (φ \land x \in X) \to (x \in X \land \sum_{k \in A} B \in ℝ)$
57	41	fvmpt2	$⊢ (x \in X \land \sum_{k \in A} B \in ℝ) \to (x \in X ⟼ \sum_{k \in A} B) (x) = \sum_{k \in A} B$
58	56 57	syl	$⊢ (φ \land x \in X) \to (x \in X ⟼ \sum_{k \in A} B) (x) = \sum_{k \in A} B$
59	58	3adant3	$⊢ (φ \land x \in X \land (x \in X ⟼ \sum_{k \in A} B) (x) = y) \to (x \in X ⟼ \sum_{k \in A} B) (x) = \sum_{k \in A} B$
60		simp3	$⊢ (φ \land x \in X \land (x \in X ⟼ \sum_{k \in A} B) (x) = y) \to (x \in X ⟼ \sum_{k \in A} B) (x) = y$
61	59 60	eqtr3d	$⊢ (φ \land x \in X \land (x \in X ⟼ \sum_{k \in A} B) (x) = y) \to \sum_{k \in A} B = y$
62	38	3adant3	$⊢ (φ \land x \in X \land (x \in X ⟼ \sum_{k \in A} B) (x) = y) \to \sum_{k \in A} B \in ℝ$
63	61 62	eqeltrrd	$⊢ (φ \land x \in X \land (x \in X ⟼ \sum_{k \in A} B) (x) = y) \to y \in ℝ$
64	63	3adant1r	$⊢ ((φ \land y \in ran (x \in X ⟼ \sum_{k \in A} B)) \land x \in X \land (x \in X ⟼ \sum_{k \in A} B) (x) = y) \to y \in ℝ$
65	64	3exp	$⊢ (φ \land y \in ran (x \in X ⟼ \sum_{k \in A} B)) \to (x \in X \to ((x \in X ⟼ \sum_{k \in A} B) (x) = y \to y \in ℝ))$
66	52 54 65	rexlimd	$⊢ (φ \land y \in ran (x \in X ⟼ \sum_{k \in A} B)) \to (\exists x \in X (x \in X ⟼ \sum_{k \in A} B) (x) = y \to y \in ℝ)$
67	49 66	mpd	$⊢ (φ \land y \in ran (x \in X ⟼ \sum_{k \in A} B)) \to y \in ℝ$
68	67	ex	$⊢ φ \to (y \in ran (x \in X ⟼ \sum_{k \in A} B) \to y \in ℝ)$
69	68	ssrdv	$⊢ φ \to ran (x \in X ⟼ \sum_{k \in A} B) \subseteq ℝ$
70	20	a1i	$⊢ φ \to ℝ \subseteq ℂ$
71		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (x \in X ⟼ \sum_{k \in A} B) \subseteq ℝ \land ℝ \subseteq ℂ) \to ((x \in X ⟼ \sum_{k \in A} B) \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in X ⟼ \sum_{k \in A} B) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
72	26 69 70 71	syl3anc	$⊢ φ \to ((x \in X ⟼ \sum_{k \in A} B) \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow (x \in X ⟼ \sum_{k \in A} B) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
73	25 72	mpbid	$⊢ φ \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
74	73 9	eleqtrrdi	$⊢ φ \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K)$

Metamath Proof Explorer

Theorem refsumcn

Proof