fsumcn

Description: A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for B normally contains free variables k and x to index it. (Contributed by NM, 8-Aug-2007) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	fsumcn.3	$⊢ K = TopOpen (ℂ_{fld})$
	fsumcn.4	$⊢ φ \to J \in TopOn (X)$
	fsumcn.5	$⊢ φ \to A \in Fin$
	fsumcn.6	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)$
Assertion	fsumcn	$⊢ φ \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		fsumcn.3	$⊢ K = TopOpen (ℂ_{fld})$
2		fsumcn.4	$⊢ φ \to J \in TopOn (X)$
3		fsumcn.5	$⊢ φ \to A \in Fin$
4		fsumcn.6	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) \in (J Cn K)$
5		ssid	$⊢ A \subseteq A$
6		sseq1	$⊢ w = \emptyset \to (w \subseteq A \leftrightarrow \emptyset \subseteq A)$
7		sumeq1	$⊢ w = \emptyset \to \sum_{k \in w} B = \sum_{k \in \emptyset} B$
8	7	mpteq2dv	$⊢ w = \emptyset \to (x \in X ⟼ \sum_{k \in w} B) = (x \in X ⟼ \sum_{k \in \emptyset} B)$
9	8	eleq1d	$⊢ w = \emptyset \to ((x \in X ⟼ \sum_{k \in w} B) \in (J Cn K) \leftrightarrow (x \in X ⟼ \sum_{k \in \emptyset} B) \in (J Cn K))$
10	6 9	imbi12d	$⊢ w = \emptyset \to ((w \subseteq A \to (x \in X ⟼ \sum_{k \in w} B) \in (J Cn K)) \leftrightarrow (\emptyset \subseteq A \to (x \in X ⟼ \sum_{k \in \emptyset} B) \in (J Cn K)))$
11	10	imbi2d	$⊢ w = \emptyset \to ((φ \to (w \subseteq A \to (x \in X ⟼ \sum_{k \in w} B) \in (J Cn K))) \leftrightarrow (φ \to (\emptyset \subseteq A \to (x \in X ⟼ \sum_{k \in \emptyset} B) \in (J Cn K))))$
12		sseq1	$⊢ w = y \to (w \subseteq A \leftrightarrow y \subseteq A)$
13		sumeq1	$⊢ w = y \to \sum_{k \in w} B = \sum_{k \in y} B$
14	13	mpteq2dv	$⊢ w = y \to (x \in X ⟼ \sum_{k \in w} B) = (x \in X ⟼ \sum_{k \in y} B)$
15	14	eleq1d	$⊢ w = y \to ((x \in X ⟼ \sum_{k \in w} B) \in (J Cn K) \leftrightarrow (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))$
16	12 15	imbi12d	$⊢ w = y \to ((w \subseteq A \to (x \in X ⟼ \sum_{k \in w} B) \in (J Cn K)) \leftrightarrow (y \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K)))$
17	16	imbi2d	$⊢ w = y \to ((φ \to (w \subseteq A \to (x \in X ⟼ \sum_{k \in w} B) \in (J Cn K))) \leftrightarrow (φ \to (y \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))))$
18		sseq1	$⊢ w = y \cup \{z\} \to (w \subseteq A \leftrightarrow y \cup \{z\} \subseteq A)$
19		sumeq1	$⊢ w = y \cup \{z\} \to \sum_{k \in w} B = \sum_{k \in y \cup \{z\}} B$
20	19	mpteq2dv	$⊢ w = y \cup \{z\} \to (x \in X ⟼ \sum_{k \in w} B) = (x \in X ⟼ \sum_{k \in y \cup \{z\}} B)$
21	20	eleq1d	$⊢ w = y \cup \{z\} \to ((x \in X ⟼ \sum_{k \in w} B) \in (J Cn K) \leftrightarrow (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K))$
22	18 21	imbi12d	$⊢ w = y \cup \{z\} \to ((w \subseteq A \to (x \in X ⟼ \sum_{k \in w} B) \in (J Cn K)) \leftrightarrow (y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K)))$
23	22	imbi2d	$⊢ w = y \cup \{z\} \to ((φ \to (w \subseteq A \to (x \in X ⟼ \sum_{k \in w} B) \in (J Cn K))) \leftrightarrow (φ \to (y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K))))$
24		sseq1	$⊢ w = A \to (w \subseteq A \leftrightarrow A \subseteq A)$
25		sumeq1	$⊢ w = A \to \sum_{k \in w} B = \sum_{k \in A} B$
26	25	mpteq2dv	$⊢ w = A \to (x \in X ⟼ \sum_{k \in w} B) = (x \in X ⟼ \sum_{k \in A} B)$
27	26	eleq1d	$⊢ w = A \to ((x \in X ⟼ \sum_{k \in w} B) \in (J Cn K) \leftrightarrow (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K))$
28	24 27	imbi12d	$⊢ w = A \to ((w \subseteq A \to (x \in X ⟼ \sum_{k \in w} B) \in (J Cn K)) \leftrightarrow (A \subseteq A \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K)))$
29	28	imbi2d	$⊢ w = A \to ((φ \to (w \subseteq A \to (x \in X ⟼ \sum_{k \in w} B) \in (J Cn K))) \leftrightarrow (φ \to (A \subseteq A \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K))))$
30		sum0	$⊢ \sum_{k \in \emptyset} B = 0$
31	30	mpteq2i	$⊢ (x \in X ⟼ \sum_{k \in \emptyset} B) = (x \in X ⟼ 0)$
32	1	cnfldtopon	$⊢ K \in TopOn (ℂ)$
33	32	a1i	$⊢ φ \to K \in TopOn (ℂ)$
34		0cnd	$⊢ φ \to 0 \in ℂ$
35	2 33 34	cnmptc	$⊢ φ \to (x \in X ⟼ 0) \in (J Cn K)$
36	31 35	eqeltrid	$⊢ φ \to (x \in X ⟼ \sum_{k \in \emptyset} B) \in (J Cn K)$
37	36	a1d	$⊢ φ \to (\emptyset \subseteq A \to (x \in X ⟼ \sum_{k \in \emptyset} B) \in (J Cn K))$
38		ssun1	$⊢ y \subseteq y \cup \{z\}$
39		sstr	$⊢ (y \subseteq y \cup \{z\} \land y \cup \{z\} \subseteq A) \to y \subseteq A$
40	38 39	mpan	$⊢ y \cup \{z\} \subseteq A \to y \subseteq A$
41	40	imim1i	$⊢ (y \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K)) \to (y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))$
42		simplr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to \neg z \in y$
43		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
44	42 43	sylibr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to y \cap \{z\} = \emptyset$
45		eqidd	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to y \cup \{z\} = y \cup \{z\}$
46	3	ad2antrr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to A \in Fin$
47		simprl	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to y \cup \{z\} \subseteq A$
48	46 47	ssfid	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to y \cup \{z\} \in Fin$
49		simplll	$⊢ (((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \land k \in (y \cup \{z\})) \to φ$
50	47	sselda	$⊢ (((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \land k \in (y \cup \{z\})) \to k \in A$
51		simplrr	$⊢ (((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \land k \in (y \cup \{z\})) \to x \in X$
52	2	adantr	$⊢ (φ \land k \in A) \to J \in TopOn (X)$
53	32	a1i	$⊢ (φ \land k \in A) \to K \in TopOn (ℂ)$
54		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (ℂ) \land (x \in X ⟼ B) \in (J Cn K)) \to (x \in X ⟼ B) : X ⟶ ℂ$
55	52 53 4 54	syl3anc	$⊢ (φ \land k \in A) \to (x \in X ⟼ B) : X ⟶ ℂ$
56		eqid	$⊢ (x \in X ⟼ B) = (x \in X ⟼ B)$
57	56	fmpt	$⊢ \forall x \in X B \in ℂ \leftrightarrow (x \in X ⟼ B) : X ⟶ ℂ$
58	55 57	sylibr	$⊢ (φ \land k \in A) \to \forall x \in X B \in ℂ$
59		rsp	$⊢ \forall x \in X B \in ℂ \to (x \in X \to B \in ℂ)$
60	58 59	syl	$⊢ (φ \land k \in A) \to (x \in X \to B \in ℂ)$
61	60	imp	$⊢ ((φ \land k \in A) \land x \in X) \to B \in ℂ$
62	49 50 51 61	syl21anc	$⊢ (((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \land k \in (y \cup \{z\})) \to B \in ℂ$
63	44 45 48 62	fsumsplit	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to \sum_{k \in y \cup \{z\}} B = \sum_{k \in y} B + \sum_{k \in \{z\}} B$
64		simpr	$⊢ ((φ \land \neg z \in y) \land y \cup \{z\} \subseteq A) \to y \cup \{z\} \subseteq A$
65	64	unssbd	$⊢ ((φ \land \neg z \in y) \land y \cup \{z\} \subseteq A) \to \{z\} \subseteq A$
66		vex	$⊢ z \in V$
67	66	snss	$⊢ z \in A \leftrightarrow \{z\} \subseteq A$
68	65 67	sylibr	$⊢ ((φ \land \neg z \in y) \land y \cup \{z\} \subseteq A) \to z \in A$
69	68	adantrr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to z \in A$
70	60	impancom	$⊢ (φ \land x \in X) \to (k \in A \to B \in ℂ)$
71	70	ralrimiv	$⊢ (φ \land x \in X) \to \forall k \in A B \in ℂ$
72	71	ad2ant2rl	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to \forall k \in A B \in ℂ$
73		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ z / k ⦌ B$
74	73	nfel1	$⊢ Ⅎ k ⦋ z / k ⦌ B \in ℂ$
75		csbeq1a	$⊢ k = z \to B = ⦋ z / k ⦌ B$
76	75	eleq1d	$⊢ k = z \to (B \in ℂ \leftrightarrow ⦋ z / k ⦌ B \in ℂ)$
77	74 76	rspc	$⊢ z \in A \to (\forall k \in A B \in ℂ \to ⦋ z / k ⦌ B \in ℂ)$
78	69 72 77	sylc	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to ⦋ z / k ⦌ B \in ℂ$
79		sumsns	$⊢ (z \in A \land ⦋ z / k ⦌ B \in ℂ) \to \sum_{k \in \{z\}} B = ⦋ z / k ⦌ B$
80	69 78 79	syl2anc	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to \sum_{k \in \{z\}} B = ⦋ z / k ⦌ B$
81	80	oveq2d	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to \sum_{k \in y} B + \sum_{k \in \{z\}} B = \sum_{k \in y} B + ⦋ z / k ⦌ B$
82	63 81	eqtrd	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land x \in X)) \to \sum_{k \in y \cup \{z\}} B = \sum_{k \in y} B + ⦋ z / k ⦌ B$
83	82	anassrs	$⊢ (((φ \land \neg z \in y) \land y \cup \{z\} \subseteq A) \land x \in X) \to \sum_{k \in y \cup \{z\}} B = \sum_{k \in y} B + ⦋ z / k ⦌ B$
84	83	mpteq2dva	$⊢ ((φ \land \neg z \in y) \land y \cup \{z\} \subseteq A) \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) = (x \in X ⟼ \sum_{k \in y} B + ⦋ z / k ⦌ B)$
85	84	adantrr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) = (x \in X ⟼ \sum_{k \in y} B + ⦋ z / k ⦌ B)$
86		nfcv	$⊢ \underline{Ⅎ} w (\sum_{k \in y} B + ⦋ z / k ⦌ B)$
87		nfcv	$⊢ \underline{Ⅎ} x y$
88		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ w / x ⦌ B$
89	87 88	nfsum	$⊢ \underline{Ⅎ} x \sum_{k \in y} ⦋ w / x ⦌ B$
90		nfcv	$⊢ \underline{Ⅎ} x +$
91		nfcv	$⊢ \underline{Ⅎ} x z$
92	91 88	nfcsbw	$⊢ \underline{Ⅎ} x ⦋ z / k ⦌ ⦋ w / x ⦌ B$
93	89 90 92	nfov	$⊢ \underline{Ⅎ} x (\sum_{k \in y} ⦋ w / x ⦌ B + ⦋ z / k ⦌ ⦋ w / x ⦌ B)$
94		csbeq1a	$⊢ x = w \to B = ⦋ w / x ⦌ B$
95	94	sumeq2sdv	$⊢ x = w \to \sum_{k \in y} B = \sum_{k \in y} ⦋ w / x ⦌ B$
96	94	csbeq2dv	$⊢ x = w \to ⦋ z / k ⦌ B = ⦋ z / k ⦌ ⦋ w / x ⦌ B$
97	95 96	oveq12d	$⊢ x = w \to \sum_{k \in y} B + ⦋ z / k ⦌ B = \sum_{k \in y} ⦋ w / x ⦌ B + ⦋ z / k ⦌ ⦋ w / x ⦌ B$
98	86 93 97	cbvmpt	$⊢ (x \in X ⟼ \sum_{k \in y} B + ⦋ z / k ⦌ B) = (w \in X ⟼ \sum_{k \in y} ⦋ w / x ⦌ B + ⦋ z / k ⦌ ⦋ w / x ⦌ B)$
99	85 98	eqtrdi	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) = (w \in X ⟼ \sum_{k \in y} ⦋ w / x ⦌ B + ⦋ z / k ⦌ ⦋ w / x ⦌ B)$
100	2	ad2antrr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to J \in TopOn (X)$
101		nfcv	$⊢ \underline{Ⅎ} w \sum_{k \in y} B$
102	101 89 95	cbvmpt	$⊢ (x \in X ⟼ \sum_{k \in y} B) = (w \in X ⟼ \sum_{k \in y} ⦋ w / x ⦌ B)$
103		simprr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K)$
104	102 103	eqeltrrid	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (w \in X ⟼ \sum_{k \in y} ⦋ w / x ⦌ B) \in (J Cn K)$
105		nfcv	$⊢ \underline{Ⅎ} w ⦋ z / k ⦌ B$
106	105 92 96	cbvmpt	$⊢ (x \in X ⟼ ⦋ z / k ⦌ B) = (w \in X ⟼ ⦋ z / k ⦌ ⦋ w / x ⦌ B)$
107	68	adantrr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to z \in A$
108	4	ralrimiva	$⊢ φ \to \forall k \in A (x \in X ⟼ B) \in (J Cn K)$
109	108	ad2antrr	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to \forall k \in A (x \in X ⟼ B) \in (J Cn K)$
110		nfcv	$⊢ \underline{Ⅎ} k X$
111	110 73	nfmpt	$⊢ \underline{Ⅎ} k (x \in X ⟼ ⦋ z / k ⦌ B)$
112	111	nfel1	$⊢ Ⅎ k (x \in X ⟼ ⦋ z / k ⦌ B) \in (J Cn K)$
113	75	mpteq2dv	$⊢ k = z \to (x \in X ⟼ B) = (x \in X ⟼ ⦋ z / k ⦌ B)$
114	113	eleq1d	$⊢ k = z \to ((x \in X ⟼ B) \in (J Cn K) \leftrightarrow (x \in X ⟼ ⦋ z / k ⦌ B) \in (J Cn K))$
115	112 114	rspc	$⊢ z \in A \to (\forall k \in A (x \in X ⟼ B) \in (J Cn K) \to (x \in X ⟼ ⦋ z / k ⦌ B) \in (J Cn K))$
116	107 109 115	sylc	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (x \in X ⟼ ⦋ z / k ⦌ B) \in (J Cn K)$
117	106 116	eqeltrrid	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (w \in X ⟼ ⦋ z / k ⦌ ⦋ w / x ⦌ B) \in (J Cn K)$
118	1	addcn	$⊢ + \in ((K \times_{t} K) Cn K)$
119	118	a1i	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to + \in ((K \times_{t} K) Cn K)$
120	100 104 117 119	cnmpt12f	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (w \in X ⟼ \sum_{k \in y} ⦋ w / x ⦌ B + ⦋ z / k ⦌ ⦋ w / x ⦌ B) \in (J Cn K)$
121	99 120	eqeltrd	$⊢ ((φ \land \neg z \in y) \land (y \cup \{z\} \subseteq A \land (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K)$
122	121	exp32	$⊢ (φ \land \neg z \in y) \to (y \cup \{z\} \subseteq A \to ((x \in X ⟼ \sum_{k \in y} B) \in (J Cn K) \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K)))$
123	122	a2d	$⊢ (φ \land \neg z \in y) \to ((y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K)) \to (y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K)))$
124	41 123	syl5	$⊢ (φ \land \neg z \in y) \to ((y \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K)) \to (y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K)))$
125	124	expcom	$⊢ \neg z \in y \to (φ \to ((y \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K)) \to (y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K))))$
126	125	adantl	$⊢ (y \in Fin \land \neg z \in y) \to (φ \to ((y \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K)) \to (y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K))))$
127	126	a2d	$⊢ (y \in Fin \land \neg z \in y) \to ((φ \to (y \subseteq A \to (x \in X ⟼ \sum_{k \in y} B) \in (J Cn K))) \to (φ \to (y \cup \{z\} \subseteq A \to (x \in X ⟼ \sum_{k \in y \cup \{z\}} B) \in (J Cn K))))$
128	11 17 23 29 37 127	findcard2s	$⊢ A \in Fin \to (φ \to (A \subseteq A \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K)))$
129	3 128	mpcom	$⊢ φ \to (A \subseteq A \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K))$
130	5 129	mpi	$⊢ φ \to (x \in X ⟼ \sum_{k \in A} B) \in (J Cn K)$

Metamath Proof Explorer

Theorem fsumcn

Proof