fsumo1

Description: The finite sum of eventually bounded functions (where the index set B does not depend on x ) is eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016) (Proof shortened by Mario Carneiro, 22-May-2016)

	Ref	Expression
Hypotheses	fsumo1.1	$⊢ φ \to A \subseteq ℝ$
	fsumo1.2	$⊢ φ \to B \in Fin$
	fsumo1.3	$⊢ (φ \land (x \in A \land k \in B)) \to C \in V$
	fsumo1.4	$⊢ (φ \land k \in B) \to (x \in A ⟼ C) \in 𝑂 (1)$
Assertion	fsumo1	$⊢ φ \to (x \in A ⟼ \sum_{k \in B} C) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		fsumo1.1	$⊢ φ \to A \subseteq ℝ$
2		fsumo1.2	$⊢ φ \to B \in Fin$
3		fsumo1.3	$⊢ (φ \land (x \in A \land k \in B)) \to C \in V$
4		fsumo1.4	$⊢ (φ \land k \in B) \to (x \in A ⟼ C) \in 𝑂 (1)$
5		ssid	$⊢ B \subseteq B$
6		sseq1	$⊢ w = \emptyset \to (w \subseteq B \leftrightarrow \emptyset \subseteq B)$
7		sumeq1	$⊢ w = \emptyset \to \sum_{k \in w} C = \sum_{k \in \emptyset} C$
8		sum0	$⊢ \sum_{k \in \emptyset} C = 0$
9	7 8	eqtrdi	$⊢ w = \emptyset \to \sum_{k \in w} C = 0$
10	9	mpteq2dv	$⊢ w = \emptyset \to (x \in A ⟼ \sum_{k \in w} C) = (x \in A ⟼ 0)$
11	10	eleq1d	$⊢ w = \emptyset \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ 0) \in 𝑂 (1))$
12	6 11	imbi12d	$⊢ w = \emptyset \to ((w \subseteq B \to (x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1)) \leftrightarrow (\emptyset \subseteq B \to (x \in A ⟼ 0) \in 𝑂 (1)))$
13	12	imbi2d	$⊢ w = \emptyset \to ((φ \to (w \subseteq B \to (x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1))) \leftrightarrow (φ \to (\emptyset \subseteq B \to (x \in A ⟼ 0) \in 𝑂 (1))))$
14		sseq1	$⊢ w = y \to (w \subseteq B \leftrightarrow y \subseteq B)$
15		sumeq1	$⊢ w = y \to \sum_{k \in w} C = \sum_{k \in y} C$
16	15	mpteq2dv	$⊢ w = y \to (x \in A ⟼ \sum_{k \in w} C) = (x \in A ⟼ \sum_{k \in y} C)$
17	16	eleq1d	$⊢ w = y \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1))$
18	14 17	imbi12d	$⊢ w = y \to ((w \subseteq B \to (x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1)) \leftrightarrow (y \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)))$
19	18	imbi2d	$⊢ w = y \to ((φ \to (w \subseteq B \to (x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1))) \leftrightarrow (φ \to (y \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1))))$
20		sseq1	$⊢ w = y \cup \{z\} \to (w \subseteq B \leftrightarrow y \cup \{z\} \subseteq B)$
21		sumeq1	$⊢ w = y \cup \{z\} \to \sum_{k \in w} C = \sum_{k \in y \cup \{z\}} C$
22	21	mpteq2dv	$⊢ w = y \cup \{z\} \to (x \in A ⟼ \sum_{k \in w} C) = (x \in A ⟼ \sum_{k \in y \cup \{z\}} C)$
23	22	eleq1d	$⊢ w = y \cup \{z\} \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1))$
24	20 23	imbi12d	$⊢ w = y \cup \{z\} \to ((w \subseteq B \to (x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1)) \leftrightarrow (y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1)))$
25	24	imbi2d	$⊢ w = y \cup \{z\} \to ((φ \to (w \subseteq B \to (x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1))) \leftrightarrow (φ \to (y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1))))$
26		sseq1	$⊢ w = B \to (w \subseteq B \leftrightarrow B \subseteq B)$
27		sumeq1	$⊢ w = B \to \sum_{k \in w} C = \sum_{k \in B} C$
28	27	mpteq2dv	$⊢ w = B \to (x \in A ⟼ \sum_{k \in w} C) = (x \in A ⟼ \sum_{k \in B} C)$
29	28	eleq1d	$⊢ w = B \to ((x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \sum_{k \in B} C) \in 𝑂 (1))$
30	26 29	imbi12d	$⊢ w = B \to ((w \subseteq B \to (x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1)) \leftrightarrow (B \subseteq B \to (x \in A ⟼ \sum_{k \in B} C) \in 𝑂 (1)))$
31	30	imbi2d	$⊢ w = B \to ((φ \to (w \subseteq B \to (x \in A ⟼ \sum_{k \in w} C) \in 𝑂 (1))) \leftrightarrow (φ \to (B \subseteq B \to (x \in A ⟼ \sum_{k \in B} C) \in 𝑂 (1))))$
32		0cn	$⊢ 0 \in ℂ$
33		o1const	$⊢ (A \subseteq ℝ \land 0 \in ℂ) \to (x \in A ⟼ 0) \in 𝑂 (1)$
34	1 32 33	sylancl	$⊢ φ \to (x \in A ⟼ 0) \in 𝑂 (1)$
35	34	a1d	$⊢ φ \to (\emptyset \subseteq B \to (x \in A ⟼ 0) \in 𝑂 (1))$
36		ssun1	$⊢ y \subseteq y \cup \{z\}$
37		sstr	$⊢ (y \subseteq y \cup \{z\} \land y \cup \{z\} \subseteq B) \to y \subseteq B$
38	36 37	mpan	$⊢ y \cup \{z\} \subseteq B \to y \subseteq B$
39	38	imim1i	$⊢ (y \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)) \to (y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1))$
40		simprl	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to \neg z \in y$
41		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
42	40 41	sylibr	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to y \cap \{z\} = \emptyset$
43	42	adantr	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to y \cap \{z\} = \emptyset$
44		eqidd	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to y \cup \{z\} = y \cup \{z\}$
45	2	adantr	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to B \in Fin$
46		simprr	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to y \cup \{z\} \subseteq B$
47	45 46	ssfid	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to y \cup \{z\} \in Fin$
48	47	adantr	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to y \cup \{z\} \in Fin$
49	46	sselda	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land k \in (y \cup \{z\})) \to k \in B$
50	49	adantlr	$⊢ (((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \land k \in (y \cup \{z\})) \to k \in B$
51	3	anass1rs	$⊢ ((φ \land k \in B) \land x \in A) \to C \in V$
52	51 4	o1mptrcl	$⊢ ((φ \land k \in B) \land x \in A) \to C \in ℂ$
53	52	an32s	$⊢ ((φ \land x \in A) \land k \in B) \to C \in ℂ$
54	53	adantllr	$⊢ (((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \land k \in B) \to C \in ℂ$
55	50 54	syldan	$⊢ (((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \land k \in (y \cup \{z\})) \to C \in ℂ$
56	43 44 48 55	fsumsplit	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{k \in y \cup \{z\}} C = \sum_{k \in y} C + \sum_{k \in \{z\}} C$
57		csbeq1a	$⊢ k = w \to C = ⦋ w / k ⦌ C$
58		nfcv	$⊢ \underline{Ⅎ} w C$
59		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ w / k ⦌ C$
60	57 58 59	cbvsum	$⊢ \sum_{k \in \{z\}} C = \sum_{w \in \{z\}} ⦋ w / k ⦌ C$
61	46	unssbd	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to \{z\} \subseteq B$
62		vex	$⊢ z \in V$
63	62	snss	$⊢ z \in B \leftrightarrow \{z\} \subseteq B$
64	61 63	sylibr	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to z \in B$
65	64	adantr	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to z \in B$
66	54	ralrimiva	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to \forall k \in B C \in ℂ$
67		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ z / k ⦌ C$
68	67	nfel1	$⊢ Ⅎ k ⦋ z / k ⦌ C \in ℂ$
69		csbeq1a	$⊢ k = z \to C = ⦋ z / k ⦌ C$
70	69	eleq1d	$⊢ k = z \to (C \in ℂ \leftrightarrow ⦋ z / k ⦌ C \in ℂ)$
71	68 70	rspc	$⊢ z \in B \to (\forall k \in B C \in ℂ \to ⦋ z / k ⦌ C \in ℂ)$
72	65 66 71	sylc	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to ⦋ z / k ⦌ C \in ℂ$
73		csbeq1	$⊢ w = z \to ⦋ w / k ⦌ C = ⦋ z / k ⦌ C$
74	73	sumsn	$⊢ (z \in B \land ⦋ z / k ⦌ C \in ℂ) \to \sum_{w \in \{z\}} ⦋ w / k ⦌ C = ⦋ z / k ⦌ C$
75	65 72 74	syl2anc	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{w \in \{z\}} ⦋ w / k ⦌ C = ⦋ z / k ⦌ C$
76	60 75	eqtrid	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{k \in \{z\}} C = ⦋ z / k ⦌ C$
77	76	oveq2d	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{k \in y} C + \sum_{k \in \{z\}} C = \sum_{k \in y} C + ⦋ z / k ⦌ C$
78	56 77	eqtrd	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{k \in y \cup \{z\}} C = \sum_{k \in y} C + ⦋ z / k ⦌ C$
79	78	mpteq2dva	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) = (x \in A ⟼ \sum_{k \in y} C + ⦋ z / k ⦌ C)$
80	1	adantr	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to A \subseteq ℝ$
81		reex	$⊢ ℝ \in V$
82	81	ssex	$⊢ A \subseteq ℝ \to A \in V$
83	80 82	syl	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to A \in V$
84		sumex	$⊢ \sum_{k \in y} C \in V$
85	84	a1i	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land x \in A) \to \sum_{k \in y} C \in V$
86		eqidd	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to (x \in A ⟼ \sum_{k \in y} C) = (x \in A ⟼ \sum_{k \in y} C)$
87		eqidd	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to (x \in A ⟼ ⦋ z / k ⦌ C) = (x \in A ⟼ ⦋ z / k ⦌ C)$
88	83 85 72 86 87	offval2	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to (x \in A ⟼ \sum_{k \in y} C) +_{f} (x \in A ⟼ ⦋ z / k ⦌ C) = (x \in A ⟼ \sum_{k \in y} C + ⦋ z / k ⦌ C)$
89	79 88	eqtr4d	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) = (x \in A ⟼ \sum_{k \in y} C) +_{f} (x \in A ⟼ ⦋ z / k ⦌ C)$
90	89	adantr	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)) \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) = (x \in A ⟼ \sum_{k \in y} C) +_{f} (x \in A ⟼ ⦋ z / k ⦌ C)$
91		id	$⊢ (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1) \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)$
92	4	ralrimiva	$⊢ φ \to \forall k \in B (x \in A ⟼ C) \in 𝑂 (1)$
93	92	adantr	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to \forall k \in B (x \in A ⟼ C) \in 𝑂 (1)$
94		nfcv	$⊢ \underline{Ⅎ} k A$
95	94 67	nfmpt	$⊢ \underline{Ⅎ} k (x \in A ⟼ ⦋ z / k ⦌ C)$
96	95	nfel1	$⊢ Ⅎ k (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝑂 (1)$
97	69	mpteq2dv	$⊢ k = z \to (x \in A ⟼ C) = (x \in A ⟼ ⦋ z / k ⦌ C)$
98	97	eleq1d	$⊢ k = z \to ((x \in A ⟼ C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝑂 (1))$
99	96 98	rspc	$⊢ z \in B \to (\forall k \in B (x \in A ⟼ C) \in 𝑂 (1) \to (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝑂 (1))$
100	64 93 99	sylc	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝑂 (1)$
101		o1add	$⊢ ((x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1) \land (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝑂 (1)) \to (x \in A ⟼ \sum_{k \in y} C) +_{f} (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝑂 (1)$
102	91 100 101	syl2anr	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)) \to (x \in A ⟼ \sum_{k \in y} C) +_{f} (x \in A ⟼ ⦋ z / k ⦌ C) \in 𝑂 (1)$
103	90 102	eqeltrd	$⊢ ((φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \land (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)) \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1)$
104	103	ex	$⊢ (φ \land (\neg z \in y \land y \cup \{z\} \subseteq B)) \to ((x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1) \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1))$
105	104	expr	$⊢ (φ \land \neg z \in y) \to (y \cup \{z\} \subseteq B \to ((x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1) \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1)))$
106	105	a2d	$⊢ (φ \land \neg z \in y) \to ((y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)) \to (y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1)))$
107	39 106	syl5	$⊢ (φ \land \neg z \in y) \to ((y \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)) \to (y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1)))$
108	107	expcom	$⊢ \neg z \in y \to (φ \to ((y \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1)) \to (y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1))))$
109	108	a2d	$⊢ \neg z \in y \to ((φ \to (y \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1))) \to (φ \to (y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1))))$
110	109	adantl	$⊢ (y \in Fin \land \neg z \in y) \to ((φ \to (y \subseteq B \to (x \in A ⟼ \sum_{k \in y} C) \in 𝑂 (1))) \to (φ \to (y \cup \{z\} \subseteq B \to (x \in A ⟼ \sum_{k \in y \cup \{z\}} C) \in 𝑂 (1))))$
111	13 19 25 31 35 110	findcard2s	$⊢ B \in Fin \to (φ \to (B \subseteq B \to (x \in A ⟼ \sum_{k \in B} C) \in 𝑂 (1)))$
112	2 111	mpcom	$⊢ φ \to (B \subseteq B \to (x \in A ⟼ \sum_{k \in B} C) \in 𝑂 (1))$
113	5 112	mpi	$⊢ φ \to (x \in A ⟼ \sum_{k \in B} C) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem fsumo1

Proof