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		simpr	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
30		mpteq1	$⊢ x = a \to (k \in x ⟼ B) = (k \in a ⟼ B)$
31	30	oveq2d	$⊢ x = a \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
32	31	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)$
33		ovex	$⊢ \underset{k \in a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in V$
34	32 33	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$
35	29 34	sylib	$⊢ (φ \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$
36	11	a1i	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
37		inss2	$⊢ 𝒫 A \cap Fin \subseteq Fin$
38		simpr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in (𝒫 A \cap Fin)$
39	37 38	sselid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in Fin$
40		nfv	$⊢ Ⅎ k a \in (𝒫 A \cap Fin)$
41	1 40	nfan	$⊢ Ⅎ k (φ \land a \in (𝒫 A \cap Fin))$
42		simpll	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to φ$
43		inss1	$⊢ 𝒫 A \cap Fin \subseteq 𝒫 A$
44	43	sseli	$⊢ a \in (𝒫 A \cap Fin) \to a \in 𝒫 A$
45	44	elpwid	$⊢ a \in (𝒫 A \cap Fin) \to a \subseteq A$
46	45	ad2antlr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to a \subseteq A$
47		simpr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to k \in a$
48	46 47	sseldd	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to k \in A$
49	42 48 3	syl2anc	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to B \in [0, +∞]$
50	49	ex	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to (k \in a \to B \in [0, +∞])$
51	41 50	ralrimi	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \forall k \in a B \in [0, +∞]$
52	10 36 39 51	gsummptcl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in [0, +∞]$
53	9 52	sselid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
54		diffi	$⊢ A \in Fin \to A ∖ a \in Fin$
55	2 54	syl	$⊢ φ \to A ∖ a \in Fin$
56	55	adantr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to A ∖ a \in Fin$
57		simpll	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in (A ∖ a)) \to φ$
58		simpr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in (A ∖ a)) \to k \in (A ∖ a)$
59	58	eldifad	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in (A ∖ a)) \to k \in A$
60	57 59 3	syl2anc	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in (A ∖ a)) \to B \in [0, +∞]$
61	60	ex	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to (k \in (A ∖ a) \to B \in [0, +∞])$
62	41 61	ralrimi	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \forall k \in (A ∖ a) B \in [0, +∞]$
63	10 36 56 62	gsummptcl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in [0, +∞]$
64	9 63	sselid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
65		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)$
66	65	simprbi	$⊢ \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in [0, +∞] \to 0 \leq \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
67	63 66	syl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to 0 \leq \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
68		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))$
69	68	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)$
70	53 64 67 69	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)$
71	70	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)$
72		simpll	$⊢ ((φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B)) \land a \in (𝒫 A \cap Fin)) \to φ$
73	45	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$
74		xrge00	$⊢ 0 = 0_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
75		xrge0plusg	$⊢ +_{𝑒} = +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
76	11	a1i	$⊢ (φ \land a \subseteq A) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
77	2	adantr	$⊢ (φ \land a \subseteq A) \to A \in Fin$
78		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
79	1 3 78	fmptdf	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
80	79	adantr	$⊢ (φ \land a \subseteq A) \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
81	78	fnmpt	$⊢ \forall k \in A B \in [0, +∞] \to (k \in A ⟼ B) Fn A$
82	14 81	syl	$⊢ φ \to (k \in A ⟼ B) Fn A$
83		c0ex	$⊢ 0 \in V$
84	83	a1i	$⊢ φ \to 0 \in V$
85	82 2 84	fndmfifsupp	$⊢ φ \to {finSupp}_{0} ((k \in A ⟼ B))$
86	85	adantr	$⊢ (φ \land a \subseteq A) \to {finSupp}_{0} ((k \in A ⟼ B))$
87		disjdif	$⊢ a \cap (A ∖ a) = \emptyset$
88	87	a1i	$⊢ (φ \land a \subseteq A) \to a \cap (A ∖ a) = \emptyset$
89		undif	$⊢ a \subseteq A \leftrightarrow a \cup (A ∖ a) = A$
90	89	biimpi	$⊢ a \subseteq A \to a \cup (A ∖ a) = A$
91	90	eqcomd	$⊢ a \subseteq A \to A = a \cup (A ∖ a)$
92	91	adantl	$⊢ (φ \land a \subseteq A) \to A = a \cup (A ∖ a)$
93	10 74 75 76 77 80 86 88 92	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)}))$
94		resmpt	$⊢ a \subseteq A \to {(k \in A ⟼ B) ↾}_{a} = (k \in a ⟼ B)$
95	94	oveq2d	$⊢ a \subseteq A \to \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{a}) = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
96	95	adantl	$⊢ (φ \land a \subseteq A) \to \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{a}) = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
97		difss	$⊢ A ∖ a \subseteq A$
98		resmpt	$⊢ A ∖ a \subseteq A \to {(k \in A ⟼ B) ↾}_{(A ∖ a)} = (k \in (A ∖ a) ⟼ B)$
99	97 98	ax-mp	$⊢ {(k \in A ⟼ B) ↾}_{(A ∖ a)} = (k \in (A ∖ a) ⟼ B)$
100	99	oveq2i	$⊢ \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{(A ∖ a)}) = \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
101	100	a1i	$⊢ (φ \land a \subseteq A) \to \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{(A ∖ a)}) = \underset{k \in A ∖ a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
102	96 101	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)$
103	93 102	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)$
104	72 73 103	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)$
105	71 104	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$
106	105	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$
107		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)$
108		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)$
109	108	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$
110	109	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$
111	107 110	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$
112	35 106 111	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$
113	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 ℝ^{*}$
114	11	a1i	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
115		simpr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in (𝒫 A \cap Fin)$
116	37 115	sselid	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in Fin$
117		nfv	$⊢ Ⅎ k x \in (𝒫 A \cap Fin)$
118	1 117	nfan	$⊢ Ⅎ k (φ \land x \in (𝒫 A \cap Fin))$
119		simpll	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to φ$
120	43	sseli	$⊢ x \in (𝒫 A \cap Fin) \to x \in 𝒫 A$
121	120	ad2antlr	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to x \in 𝒫 A$
122	121	elpwid	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to x \subseteq A$
123		simpr	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to k \in x$
124	122 123	sseldd	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to k \in A$
125	119 124 3	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B \in [0, +∞]$
126	125	ex	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to (k \in x \to B \in [0, +∞])$
127	118 126	ralrimi	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \forall k \in x B \in [0, +∞]$
128	10 114 116 127	gsummptcl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in [0, +∞]$
129	9 128	sselid	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
130	129	ralrimiva	$⊢ φ \to \forall x \in (𝒫 A \cap Fin) \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
131	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 ℝ^{}$
132	130 131	syl	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \subseteq ℝ^{}$
133	132	sselda	$⊢ (φ \land y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)) \to y \in ℝ^{}$
134		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)$
135	134	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)$
136	113 133 135	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)$
137	112 136	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$
138	8 16 28 137	supmax	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) ℝ^{} <) = \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
139	6 138	eqtr2d	$⊢ φ \to \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in A}{\sum^{}} B$

Metamath Proof Explorer

Theorem gsumesum

Proof