gsumesum

Description: Relate a group sum on ` ( RR*s |``s ( 0 , +oo ) ) ` to a finite extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017) (Proof shortened by AV, 12-Dec-2019)

	Ref	Expression
Hypotheses	gsumesum.0	$⊢ Ⅎ k φ$
	gsumesum.1	$⊢ φ \to A \in Fin$
	gsumesum.2	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
Assertion	gsumesum	$⊢ φ \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in A}{\sum^{}} B$

Proof

Step	Hyp	Ref	Expression
1		gsumesum.0	$⊢ Ⅎ k φ$
2		gsumesum.1	$⊢ φ \to A \in Fin$
3		gsumesum.2	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
4		nfcv	$⊢ \underline{Ⅎ} k A$
5		eqidd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
6	1 4 2 3 5	esumval	$⊢ φ \to \underset{k \in A}{\sum^{}} B = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) ℝ^{*} <)$
7		xrltso	$⊢ < Or ℝ^{*}$
8	7	a1i	$⊢ φ \to < Or ℝ^{*}$
9		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
10		xrge0base	$⊢ [0, +∞] = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
11		xrge0cmn	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
12	11	a1i	$⊢ φ \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
13	3	ex	$⊢ φ \to (k \in A \to B \in [0, +∞])$
14	1 13	ralrimi	$⊢ φ \to \forall k \in A B \in [0, +∞]$
15	10 12 2 14	gsummptcl	$⊢ φ \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in [0, +∞]$
16	9 15	sselid	$⊢ φ \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
17		pwidg	$⊢ A \in Fin \to A \in 𝒫 A$
18	2 17	syl	$⊢ φ \to A \in 𝒫 A$
19	18 2	elind	$⊢ φ \to A \in (𝒫 A \cap Fin)$
20		eqidd	$⊢ φ \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
21		mpteq1	$⊢ x = A \to (k \in x ⟼ B) = (k \in A ⟼ B)$
22	21	oveq2d	$⊢ x = A \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
23	22	rspceeqv	$⊢ (A \in (𝒫 A \cap Fin) \land \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \to \exists x \in (𝒫 A \cap Fin) \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
24	19 20 23	syl2anc	$⊢ φ \to \exists x \in (𝒫 A \cap Fin) \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
25		eqid	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) = (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
26		ovex	$⊢ \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in V$
27	25 26	elrnmpti	$⊢ \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \leftrightarrow \exists x \in (𝒫 A \cap Fin) \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
28	24 27	sylibr	$⊢ φ \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
29		mpteq1	$⊢ x = a \to (k \in x ⟼ B) = (k \in a ⟼ B)$
30	29	oveq2d	$⊢ x = a \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
31	30	cbvmptv	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) = (a \in (𝒫 A \cap Fin) ⟼ \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
32		ovex	$⊢ \underset{k \in a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in V$
33	31 32	elrnmpti	$⊢ y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \leftrightarrow \exists a \in (𝒫 A \cap Fin) y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
34	33	bilani	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to \exists a \in (𝒫 A \cap Fin) y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
35	11	a1i	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
36		inss2	$⊢ 𝒫 A \cap Fin \subseteq Fin$
37		simpr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in (𝒫 A \cap Fin)$
38	36 37	sselid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in Fin$
39		nfv	$⊢ Ⅎ k a \in (𝒫 A \cap Fin)$
40	1 39	nfan	$⊢ Ⅎ k (φ \land a \in (𝒫 A \cap Fin))$
41		simpll	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to φ$
42		inss1	$⊢ 𝒫 A \cap Fin \subseteq 𝒫 A$
43	42	sseli	$⊢ a \in (𝒫 A \cap Fin) \to a \in 𝒫 A$
44	43	elpwid	$⊢ a \in (𝒫 A \cap Fin) \to a \subseteq A$
45	44	ad2antlr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to a \subseteq A$
46		simpr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to k \in a$
47	45 46	sseldd	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to k \in A$
48	41 47 3	syl2anc	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to B \in [0, +∞]$
49	48	ex	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to (k \in a \to B \in [0, +∞])$
50	40 49	ralrimi	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \forall k \in a B \in [0, +∞]$
51	10 35 38 50	gsummptcl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in [0, +∞]$
52	9 51	sselid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
53		diffi	$⊢ A \in Fin \to A ∖ a \in Fin$
54	2 53	syl	$⊢ φ \to A ∖ a \in Fin$
55	54	adantr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to A ∖ a \in Fin$
56		simpll	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in (A ∖ a)) \to φ$
57		simpr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in (A ∖ a)) \to k \in (A ∖ a)$
58	57	eldifad	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in (A ∖ a)) \to k \in A$
59	56 58 3	syl2anc	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in (A ∖ a)) \to B \in [0, +∞]$
60	59	ex	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to (k \in (A ∖ a) \to B \in [0, +∞])$
61	40 60	ralrimi	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \forall k \in (A ∖ a) B \in [0, +∞]$
62	10 35 55 61	gsummptcl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in [0, +∞]$
63	9 62	sselid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
64		elxrge0	$⊢ \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in [0, +∞] \leftrightarrow (\underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{} \land 0 \leq \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
65	64	simprbi	$⊢ \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in [0, +∞] \to 0 \leq \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
66	62 65	syl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to 0 \leq \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
67		xraddge02	$⊢ (\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{} \land \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}) \to (0 \leq \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq (\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B) +_{𝑒} (\underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B))$
68	67	imp	$⊢ ((\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{} \land \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}) \land 0 \leq \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq (\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B) +_{𝑒} (\underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B)$
69	52 63 66 68	syl21anc	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq (\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B) +_{𝑒} (\underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}}, B)$
70	69	adantlr	$⊢ ((φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq (\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B) +_{𝑒} (\underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B)$
71		simpll	$⊢ ((φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B)) \land a \in (𝒫 A \cap Fin)) \to φ$
72	44	adantl	$⊢ ((φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B)) \land a \in (𝒫 A \cap Fin)) \to a \subseteq A$
73		xrge00	$⊢ 0 = 0_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
74		xrge0plusg	$⊢ +_{𝑒} = +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
75	11	a1i	$⊢ (φ \land a \subseteq A) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
76	2	adantr	$⊢ (φ \land a \subseteq A) \to A \in Fin$
77		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
78	1 3 77	fmptdf	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
79	78	adantr	$⊢ (φ \land a \subseteq A) \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
80	77	fnmpt	$⊢ \forall k \in A B \in [0, +∞] \to (k \in A ⟼ B) Fn A$
81	14 80	syl	$⊢ φ \to (k \in A ⟼ B) Fn A$
82		c0ex	$⊢ 0 \in V$
83	82	a1i	$⊢ φ \to 0 \in V$
84	81 2 83	fndmfifsupp	$⊢ φ \to {finSupp}_{0} ((k \in A ⟼ B))$
85	84	adantr	$⊢ (φ \land a \subseteq A) \to {finSupp}_{0} ((k \in A ⟼ B))$
86		disjdif	$⊢ a \cap (A ∖ a) = \emptyset$
87	86	a1i	$⊢ (φ \land a \subseteq A) \to a \cap (A ∖ a) = \emptyset$
88		undif	$⊢ a \subseteq A \leftrightarrow a \cup (A ∖ a) = A$
89	88	biimpi	$⊢ a \subseteq A \to a \cup (A ∖ a) = A$
90	89	eqcomd	$⊢ a \subseteq A \to A = a \cup (A ∖ a)$
91	90	adantl	$⊢ (φ \land a \subseteq A) \to A = a \cup (A ∖ a)$
92	10 73 74 75 76 79 85 87 91	gsumsplit	$⊢ (φ \land a \subseteq A) \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = (\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}, ({(k \in A ⟼ B) ↾}_{a})) +_{𝑒} (\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}, ({(k \in A ⟼ B) ↾}_{(A ∖ a)}))$
93		resmpt	$⊢ a \subseteq A \to {(k \in A ⟼ B) ↾}_{a} = (k \in a ⟼ B)$
94	93	oveq2d	$⊢ a \subseteq A \to \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{a}) = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
95	94	adantl	$⊢ (φ \land a \subseteq A) \to \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{a}) = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
96		difss	$⊢ A ∖ a \subseteq A$
97		resmpt	$⊢ A ∖ a \subseteq A \to {(k \in A ⟼ B) ↾}_{(A ∖ a)} = (k \in (A ∖ a) ⟼ B)$
98	96 97	ax-mp	$⊢ {(k \in A ⟼ B) ↾}_{(A ∖ a)} = (k \in (A ∖ a) ⟼ B)$
99	98	oveq2i	$⊢ \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{(A ∖ a)}) = \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
100	99	a1i	$⊢ (φ \land a \subseteq A) \to \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{(A ∖ a)}) = \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
101	95 100	oveq12d	$⊢ (φ \land a \subseteq A) \to (\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}, ({(k \in A ⟼ B) ↾}_{a})) +_{𝑒} (\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}, ({(k \in A ⟼ B) ↾}_{(A ∖ a)})) = (\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B) +_{𝑒} (\underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B)$
102	92 101	eqtrd	$⊢ (φ \land a \subseteq A) \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = (\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B) +_{𝑒} (\underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}}, B)$
103	71 72 102	syl2anc	$⊢ ((φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \land a \in (𝒫 A \cap Fin)) \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = (\underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B) +_{𝑒} (\underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, B)$
104	70 103	breqtrrd	$⊢ ((φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
105	104	ralrimiva	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to \forall a \in (𝒫 A \cap Fin) \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
106		r19.29r	$⊢ (\exists a \in (𝒫 A \cap Fin) y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \land \forall a \in (𝒫 A \cap Fin) \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \to \exists a \in (𝒫 A \cap Fin) (y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \land \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
107		breq1	$⊢ y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \to (y \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leftrightarrow \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
108	107	biimpar	$⊢ (y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \land \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \to y \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
109	108	rexlimivw	$⊢ \exists a \in (𝒫 A \cap Fin) (y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \land \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \to y \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
110	106 109	syl	$⊢ (\exists a \in (𝒫 A \cap Fin) y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \land \forall a \in (𝒫 A \cap Fin) \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \to y \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
111	34 105 110	syl2anc	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to y \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
112	16	adantr	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{*}$
113	11	a1i	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
114		simpr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in (𝒫 A \cap Fin)$
115	36 114	sselid	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in Fin$
116		nfv	$⊢ Ⅎ k x \in (𝒫 A \cap Fin)$
117	1 116	nfan	$⊢ Ⅎ k (φ \land x \in (𝒫 A \cap Fin))$
118		simpll	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to φ$
119	42	sseli	$⊢ x \in (𝒫 A \cap Fin) \to x \in 𝒫 A$
120	119	ad2antlr	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to x \in 𝒫 A$
121	120	elpwid	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to x \subseteq A$
122		simpr	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to k \in x$
123	121 122	sseldd	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to k \in A$
124	118 123 3	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B \in [0, +∞]$
125	124	ex	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to (k \in x \to B \in [0, +∞])$
126	117 125	ralrimi	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \forall k \in x B \in [0, +∞]$
127	10 113 115 126	gsummptcl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in [0, +∞]$
128	9 127	sselid	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
129	128	ralrimiva	$⊢ φ \to \forall x \in (𝒫 A \cap Fin) \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
130	25	rnmptss	$⊢ \forall x \in (𝒫 A \cap Fin) \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{} \to ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \subseteq ℝ^{}$
131	129 130	syl	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \subseteq ℝ^{}$
132	131	sselda	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to y \in ℝ^{}$
133		xrltnle	$⊢ (\underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{} \land y \in ℝ^{}) \to (\underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B < y \leftrightarrow \neg y \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B)$
134	133	con2bid	$⊢ (\underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{} \land y \in ℝ^{}) \to (y \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leftrightarrow \neg \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B < y)$
135	112 132 134	syl2anc	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to (y \leq \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leftrightarrow \neg \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B < y)$
136	111 135	mpbid	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to \neg \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B < y$
137	8 16 28 136	supmax	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) ℝ^{} <) = \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
138	6 137	eqtr2d	$⊢ φ \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in A}{\sum^{}} B$

Metamath Proof Explorer

Theorem gsumesum

Proof