sge0resplit

Description: sum^ splits into two parts, when it's a real number. This is a special case of sge0split . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0resplit.a	$⊢ φ \to A \in V$
	sge0resplit.b	$⊢ φ \to B \in W$
	sge0resplit.u	$⊢ U = A \cup B$
	sge0resplit.in0	$⊢ φ \to A \cap B = \emptyset$
	sge0resplit.f	$⊢ φ \to F : U ⟶ [0, +∞]$
	sge0resplit.re	$⊢ φ \to sum^(F) \in ℝ$
Assertion	sge0resplit	$⊢ φ \to sum^(F) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		sge0resplit.a	$⊢ φ \to A \in V$
2		sge0resplit.b	$⊢ φ \to B \in W$
3		sge0resplit.u	$⊢ U = A \cup B$
4		sge0resplit.in0	$⊢ φ \to A \cap B = \emptyset$
5		sge0resplit.f	$⊢ φ \to F : U ⟶ [0, +∞]$
6		sge0resplit.re	$⊢ φ \to sum^(F) \in ℝ$
7		ssun1	$⊢ A \subseteq A \cup B$
8	3	eqcomi	$⊢ A \cup B = U$
9	7 8	sseqtri	$⊢ A \subseteq U$
10	9	a1i	$⊢ φ \to A \subseteq U$
11	5 10	fssresd	$⊢ φ \to ({F ↾}_{A}) : A ⟶ [0, +∞]$
12	3	a1i	$⊢ φ \to U = A \cup B$
13		unexg	$⊢ (A \in V \land B \in W) \to A \cup B \in V$
14	1 2 13	syl2anc	$⊢ φ \to A \cup B \in V$
15	12 14	eqeltrd	$⊢ φ \to U \in V$
16	15 5 6	sge0ssre	$⊢ φ \to sum^({F ↾}_{A}) \in ℝ$
17	1 11 16	sge0supre	$⊢ φ \to sum^({F ↾}_{A}) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <)$
18	17 16	eqeltrrd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) \in ℝ$
19		ssun2	$⊢ B \subseteq A \cup B$
20	19 8	sseqtri	$⊢ B \subseteq U$
21	20	a1i	$⊢ φ \to B \subseteq U$
22	5 21	fssresd	$⊢ φ \to ({F ↾}_{B}) : B ⟶ [0, +∞]$
23	15 5 6	sge0ssre	$⊢ φ \to sum^({F ↾}_{B}) \in ℝ$
24	2 22 23	sge0supre	$⊢ φ \to sum^({F ↾}_{B}) = sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <)$
25	24 23	eqeltrrd	$⊢ φ \to sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <) \in ℝ$
26		rexadd	$⊢ (sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) \in ℝ \land sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <) \in ℝ) \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) +_{𝑒} sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) + sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <)$
27	18 25 26	syl2anc	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) +_{𝑒} sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) + sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <)$
28	15 5 6	sge0rern	$⊢ φ \to \neg +∞ \in ran F$
29		nelrnres	$⊢ \neg +∞ \in ran F \to \neg +∞ \in ran ({F ↾}_{A})$
30	28 29	syl	$⊢ φ \to \neg +∞ \in ran ({F ↾}_{A})$
31	11 30	fge0iccico	$⊢ φ \to ({F ↾}_{A}) : A ⟶ [0, +∞)$
32	31	sge0rnre	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \subseteq ℝ$
33		sge0rnn0	$⊢ ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \neq \emptyset$
34	33	a1i	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \neq \emptyset$
35	1 31	sge0reval	$⊢ φ \to sum^({F ↾}_{A}) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ^{*} <)$
36	35	eqcomd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ^{*} <) = sum^({F ↾}_{A})$
37	36 16	eqeltrd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ^{*} <) \in ℝ$
38		supxrre3	$⊢ (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \subseteq ℝ \land ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \neq \emptyset) \to (sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ^{*} <) \in ℝ \leftrightarrow \exists w \in ℝ \forall t \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) t \leq w)$
39	32 34 38	syl2anc	$⊢ φ \to (sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ^{*} <) \in ℝ \leftrightarrow \exists w \in ℝ \forall t \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) t \leq w)$
40	37 39	mpbid	$⊢ φ \to \exists w \in ℝ \forall t \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) t \leq w$
41		nelrnres	$⊢ \neg +∞ \in ran F \to \neg +∞ \in ran ({F ↾}_{B})$
42	28 41	syl	$⊢ φ \to \neg +∞ \in ran ({F ↾}_{B})$
43	22 42	fge0iccico	$⊢ φ \to ({F ↾}_{B}) : B ⟶ [0, +∞)$
44	43	sge0rnre	$⊢ φ \to ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \subseteq ℝ$
45		sge0rnn0	$⊢ ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \neq \emptyset$
46	45	a1i	$⊢ φ \to ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \neq \emptyset$
47	2 43	sge0reval	$⊢ φ \to sum^({F ↾}_{B}) = sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ^{*} <)$
48	47	eqcomd	$⊢ φ \to sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ^{*} <) = sum^({F ↾}_{B})$
49	48 23	eqeltrd	$⊢ φ \to sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ^{*} <) \in ℝ$
50		supxrre3	$⊢ (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \subseteq ℝ \land ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \neq \emptyset) \to (sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ^{*} <) \in ℝ \leftrightarrow \exists w \in ℝ \forall t \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) t \leq w)$
51	44 46 50	syl2anc	$⊢ φ \to (sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ^{*} <) \in ℝ \leftrightarrow \exists w \in ℝ \forall t \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) t \leq w)$
52	49 51	mpbid	$⊢ φ \to \exists w \in ℝ \forall t \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) t \leq w$
53		eqid	$⊢ \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} = \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\}$
54	32 34 40 44 46 52 53	supadd	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) + sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <) = sup (\{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} ℝ <)$
55		simpl	$⊢ (φ \land r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\}) \to φ$
56		vex	$⊢ r \in V$
57		eqeq1	$⊢ z = r \to (z = v + u \leftrightarrow r = v + u)$
58	57	rexbidv	$⊢ z = r \to (\exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u \leftrightarrow \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u)$
59	58	rexbidv	$⊢ z = r \to (\exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u \leftrightarrow \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u)$
60	56 59	elab	$⊢ r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} \leftrightarrow \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
61	60	biimpi	$⊢ r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} \to \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
62	61	adantl	$⊢ (φ \land r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\}) \to \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
63		simpl	$⊢ (φ \land (v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)))) \to φ$
64		vex	$⊢ v \in V$
65		sumeq1	$⊢ x = a \to \sum_{y \in x} ({F ↾}_{A}) (y) = \sum_{y \in a} ({F ↾}_{A}) (y)$
66	65	cbvmptv	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) = (a \in (𝒫 A \cap Fin) ⟼ \sum_{y \in a} ({F ↾}_{A}) (y))$
67	66	elrnmpt	$⊢ v \in V \to (v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \leftrightarrow \exists a \in (𝒫 A \cap Fin) v = \sum_{y \in a} ({F ↾}_{A}) (y))$
68	64 67	ax-mp	$⊢ v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \leftrightarrow \exists a \in (𝒫 A \cap Fin) v = \sum_{y \in a} ({F ↾}_{A}) (y)$
69	68	biimpi	$⊢ v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \to \exists a \in (𝒫 A \cap Fin) v = \sum_{y \in a} ({F ↾}_{A}) (y)$
70	69	adantr	$⊢ (v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))) \to \exists a \in (𝒫 A \cap Fin) v = \sum_{y \in a} ({F ↾}_{A}) (y)$
71		vex	$⊢ u \in V$
72		sumeq1	$⊢ x = b \to \sum_{y \in x} ({F ↾}_{B}) (y) = \sum_{y \in b} ({F ↾}_{B}) (y)$
73	72	cbvmptv	$⊢ (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) = (b \in (𝒫 B \cap Fin) ⟼ \sum_{y \in b} ({F ↾}_{B}) (y))$
74	73	elrnmpt	$⊢ u \in V \to (u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \leftrightarrow \exists b \in (𝒫 B \cap Fin) u = \sum_{y \in b} ({F ↾}_{B}) (y))$
75	71 74	ax-mp	$⊢ u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \leftrightarrow \exists b \in (𝒫 B \cap Fin) u = \sum_{y \in b} ({F ↾}_{B}) (y)$
76	75	biimpi	$⊢ u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \to \exists b \in (𝒫 B \cap Fin) u = \sum_{y \in b} ({F ↾}_{B}) (y)$
77	76	adantl	$⊢ (v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))) \to \exists b \in (𝒫 B \cap Fin) u = \sum_{y \in b} ({F ↾}_{B}) (y)$
78	70 77	jca	$⊢ (v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))) \to (\exists a \in (𝒫 A \cap Fin) v = \sum_{y \in a} ({F ↾}_{A}) (y) \land \exists b \in (𝒫 B \cap Fin) u = \sum_{y \in b} ({F ↾}_{B}) (y))$
79		reeanv	$⊢ \exists a \in (𝒫 A \cap Fin) \exists b \in (𝒫 B \cap Fin) (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y)) \leftrightarrow (\exists a \in (𝒫 A \cap Fin) v = \sum_{y \in a} ({F ↾}_{A}) (y) \land \exists b \in (𝒫 B \cap Fin) u = \sum_{y \in b} ({F ↾}_{B}) (y))$
80	78 79	sylibr	$⊢ (v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))) \to \exists a \in (𝒫 A \cap Fin) \exists b \in (𝒫 B \cap Fin) (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))$
81	80	adantl	$⊢ (φ \land (v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)))) \to \exists a \in (𝒫 A \cap Fin) \exists b \in (𝒫 B \cap Fin) (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))$
82		eqid	$⊢ (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
83		elinel1	$⊢ a \in (𝒫 A \cap Fin) \to a \in 𝒫 A$
84		elpwi	$⊢ a \in 𝒫 A \to a \subseteq A$
85		id	$⊢ a \subseteq A \to a \subseteq A$
86	85 9	sstrdi	$⊢ a \subseteq A \to a \subseteq U$
87	84 86	syl	$⊢ a \in 𝒫 A \to a \subseteq U$
88	83 87	syl	$⊢ a \in (𝒫 A \cap Fin) \to a \subseteq U$
89	88	adantr	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \subseteq U$
90		elinel1	$⊢ b \in (𝒫 B \cap Fin) \to b \in 𝒫 B$
91		elpwi	$⊢ b \in 𝒫 B \to b \subseteq B$
92		id	$⊢ b \subseteq B \to b \subseteq B$
93	92 20	sstrdi	$⊢ b \subseteq B \to b \subseteq U$
94	91 93	syl	$⊢ b \in 𝒫 B \to b \subseteq U$
95	90 94	syl	$⊢ b \in (𝒫 B \cap Fin) \to b \subseteq U$
96	95	adantl	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to b \subseteq U$
97	89 96	unssd	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \cup b \subseteq U$
98		vex	$⊢ a \in V$
99		vex	$⊢ b \in V$
100	98 99	unex	$⊢ a \cup b \in V$
101	100	elpw	$⊢ a \cup b \in 𝒫 U \leftrightarrow a \cup b \subseteq U$
102	97 101	sylibr	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \cup b \in 𝒫 U$
103		elinel2	$⊢ a \in (𝒫 A \cap Fin) \to a \in Fin$
104	103	adantr	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \in Fin$
105		elinel2	$⊢ b \in (𝒫 B \cap Fin) \to b \in Fin$
106	105	adantl	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to b \in Fin$
107		unfi	$⊢ (a \in Fin \land b \in Fin) \to a \cup b \in Fin$
108	104 106 107	syl2anc	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \cup b \in Fin$
109	102 108	elind	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \cup b \in (𝒫 U \cap Fin)$
110	109	adantl	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \cup b \in (𝒫 U \cap Fin)$
111	110	ad2antrr	$⊢ (((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \land r = v + u) \to a \cup b \in (𝒫 U \cap Fin)$
112		simpl	$⊢ (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y)) \to v = \sum_{y \in a} ({F ↾}_{A}) (y)$
113		simpr	$⊢ (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y)) \to u = \sum_{y \in b} ({F ↾}_{B}) (y)$
114	112 113	oveq12d	$⊢ (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y)) \to v + u = \sum_{y \in a} ({F ↾}_{A}) (y) + \sum_{y \in b} ({F ↾}_{B}) (y)$
115	114	adantl	$⊢ ((a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \to v + u = \sum_{y \in a} ({F ↾}_{A}) (y) + \sum_{y \in b} ({F ↾}_{B}) (y)$
116	83 84	syl	$⊢ a \in (𝒫 A \cap Fin) \to a \subseteq A$
117	116	sselda	$⊢ (a \in (𝒫 A \cap Fin) \land y \in a) \to y \in A$
118		fvres	$⊢ y \in A \to ({F ↾}_{A}) (y) = F (y)$
119	117 118	syl	$⊢ (a \in (𝒫 A \cap Fin) \land y \in a) \to ({F ↾}_{A}) (y) = F (y)$
120	119	sumeq2dv	$⊢ a \in (𝒫 A \cap Fin) \to \sum_{y \in a} ({F ↾}_{A}) (y) = \sum_{y \in a} F (y)$
121	120	adantr	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to \sum_{y \in a} ({F ↾}_{A}) (y) = \sum_{y \in a} F (y)$
122	90 91	syl	$⊢ b \in (𝒫 B \cap Fin) \to b \subseteq B$
123	122	sselda	$⊢ (b \in (𝒫 B \cap Fin) \land y \in b) \to y \in B$
124		fvres	$⊢ y \in B \to ({F ↾}_{B}) (y) = F (y)$
125	123 124	syl	$⊢ (b \in (𝒫 B \cap Fin) \land y \in b) \to ({F ↾}_{B}) (y) = F (y)$
126	125	sumeq2dv	$⊢ b \in (𝒫 B \cap Fin) \to \sum_{y \in b} ({F ↾}_{B}) (y) = \sum_{y \in b} F (y)$
127	126	adantl	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to \sum_{y \in b} ({F ↾}_{B}) (y) = \sum_{y \in b} F (y)$
128	121 127	oveq12d	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to \sum_{y \in a} ({F ↾}_{A}) (y) + \sum_{y \in b} ({F ↾}_{B}) (y) = \sum_{y \in a} F (y) + \sum_{y \in b} F (y)$
129	128	adantr	$⊢ ((a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \to \sum_{y \in a} ({F ↾}_{A}) (y) + \sum_{y \in b} ({F ↾}_{B}) (y) = \sum_{y \in a} F (y) + \sum_{y \in b} F (y)$
130	115 129	eqtrd	$⊢ ((a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \to v + u = \sum_{y \in a} F (y) + \sum_{y \in b} F (y)$
131	130	ad4ant23	$⊢ (((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \land r = v + u) \to v + u = \sum_{y \in a} F (y) + \sum_{y \in b} F (y)$
132		simpr	$⊢ (((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \land r = v + u) \to r = v + u$
133	4	adantr	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to A \cap B = \emptyset$
134	116	ad2antrl	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \subseteq A$
135	122	adantl	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to b \subseteq B$
136	135	adantl	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to b \subseteq B$
137		ssin0	$⊢ (A \cap B = \emptyset \land a \subseteq A \land b \subseteq B) \to a \cap b = \emptyset$
138	133 134 136 137	syl3anc	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \cap b = \emptyset$
139		eqidd	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \cup b = a \cup b$
140	108	adantl	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \cup b \in Fin$
141		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
142		ax-resscn	$⊢ ℝ \subseteq ℂ$
143	141 142	sstri	$⊢ [0, +∞) \subseteq ℂ$
144	5 28	fge0iccico	$⊢ φ \to F : U ⟶ [0, +∞)$
145	144	ad2antrr	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land y \in (a \cup b)) \to F : U ⟶ [0, +∞)$
146	97	sselda	$⊢ ((a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \land y \in (a \cup b)) \to y \in U$
147	146	adantll	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land y \in (a \cup b)) \to y \in U$
148	145 147	ffvelcdmd	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land y \in (a \cup b)) \to F (y) \in [0, +∞)$
149	143 148	sselid	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land y \in (a \cup b)) \to F (y) \in ℂ$
150	138 139 140 149	fsumsplit	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to \sum_{y \in a \cup b} F (y) = \sum_{y \in a} F (y) + \sum_{y \in b} F (y)$
151	150	ad2antrr	$⊢ (((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \land r = v + u) \to \sum_{y \in a \cup b} F (y) = \sum_{y \in a} F (y) + \sum_{y \in b} F (y)$
152	131 132 151	3eqtr4d	$⊢ (((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \land r = v + u) \to r = \sum_{y \in a \cup b} F (y)$
153		sumeq1	$⊢ x = a \cup b \to \sum_{y \in x} F (y) = \sum_{y \in a \cup b} F (y)$
154	153	rspceeqv	$⊢ (a \cup b \in (𝒫 U \cap Fin) \land r = \sum_{y \in a \cup b} F (y)) \to \exists x \in (𝒫 U \cap Fin) r = \sum_{y \in x} F (y)$
155	111 152 154	syl2anc	$⊢ (((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \land r = v + u) \to \exists x \in (𝒫 U \cap Fin) r = \sum_{y \in x} F (y)$
156	56	a1i	$⊢ (((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \land r = v + u) \to r \in V$
157	82 155 156	elrnmptd	$⊢ (((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \land r = v + u) \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
158	157	ex	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \to (r = v + u \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
159	158	ex	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to ((v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y)) \to (r = v + u \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))))$
160	159	ex	$⊢ φ \to ((a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to ((v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y)) \to (r = v + u \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))))$
161	160	rexlimdvv	$⊢ φ \to (\exists a \in (𝒫 A \cap Fin) \exists b \in (𝒫 B \cap Fin) (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y)) \to (r = v + u \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))))$
162	161	imp	$⊢ (φ \land \exists a \in (𝒫 A \cap Fin) \exists b \in (𝒫 B \cap Fin) (v = \sum_{y \in a} ({F ↾}_{A}) (y) \land u = \sum_{y \in b} ({F ↾}_{B}) (y))) \to (r = v + u \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
163	63 81 162	syl2anc	$⊢ (φ \land (v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)))) \to (r = v + u \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
164	163	ex	$⊢ φ \to ((v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))) \to (r = v + u \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))))$
165	164	rexlimdvv	$⊢ φ \to (\exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
166	165	imp	$⊢ (φ \land \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u) \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
167	55 62 166	syl2anc	$⊢ (φ \land r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\}) \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
168	167	ex	$⊢ φ \to (r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} \to r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
169	82	elrnmpt	$⊢ r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \to (r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \leftrightarrow \exists x \in (𝒫 U \cap Fin) r = \sum_{y \in x} F (y))$
170	169	ibi	$⊢ r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \to \exists x \in (𝒫 U \cap Fin) r = \sum_{y \in x} F (y)$
171	170	adantl	$⊢ (φ \land r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))) \to \exists x \in (𝒫 U \cap Fin) r = \sum_{y \in x} F (y)$
172		nfv	$⊢ Ⅎ x φ$
173		nfcv	$⊢ \underline{Ⅎ} x r$
174		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
175	174	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
176	173 175	nfel	$⊢ Ⅎ x r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
177	172 176	nfan	$⊢ Ⅎ x (φ \land r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
178		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y))$
179	178	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y))$
180		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))$
181	180	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))$
182		nfv	$⊢ Ⅎ x r = v + u$
183	181 182	nfrexw	$⊢ Ⅎ x \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
184	179 183	nfrexw	$⊢ Ⅎ x \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
185		inss2	$⊢ x \cap A \subseteq A$
186	185	sseli	$⊢ y \in (x \cap A) \to y \in A$
187	186	adantl	$⊢ (x \in (𝒫 U \cap Fin) \land y \in (x \cap A)) \to y \in A$
188	118	eqcomd	$⊢ y \in A \to F (y) = ({F ↾}_{A}) (y)$
189	187 188	syl	$⊢ (x \in (𝒫 U \cap Fin) \land y \in (x \cap A)) \to F (y) = ({F ↾}_{A}) (y)$
190	189	sumeq2dv	$⊢ x \in (𝒫 U \cap Fin) \to \sum_{y \in x \cap A} F (y) = \sum_{y \in x \cap A} ({F ↾}_{A}) (y)$
191		sumeq1	$⊢ x = z \to \sum_{y \in x} ({F ↾}_{A}) (y) = \sum_{y \in z} ({F ↾}_{A}) (y)$
192	191	cbvmptv	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) = (z \in (𝒫 A \cap Fin) ⟼ \sum_{y \in z} ({F ↾}_{A}) (y))$
193		vex	$⊢ x \in V$
194	193	inex1	$⊢ x \cap A \in V$
195	194	elpw	$⊢ x \cap A \in 𝒫 A \leftrightarrow x \cap A \subseteq A$
196	185 195	mpbir	$⊢ x \cap A \in 𝒫 A$
197	196	a1i	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \in 𝒫 A$
198		elinel2	$⊢ x \in (𝒫 U \cap Fin) \to x \in Fin$
199		inss1	$⊢ x \cap A \subseteq x$
200	199	a1i	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \subseteq x$
201		ssfi	$⊢ (x \in Fin \land x \cap A \subseteq x) \to x \cap A \in Fin$
202	198 200 201	syl2anc	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \in Fin$
203	197 202	elind	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \in (𝒫 A \cap Fin)$
204		eqidd	$⊢ x \in (𝒫 U \cap Fin) \to \sum_{y \in x \cap A} ({F ↾}_{A}) (y) = \sum_{y \in x \cap A} ({F ↾}_{A}) (y)$
205		sumeq1	$⊢ z = x \cap A \to \sum_{y \in z} ({F ↾}_{A}) (y) = \sum_{y \in x \cap A} ({F ↾}_{A}) (y)$
206	205	rspceeqv	$⊢ (x \cap A \in (𝒫 A \cap Fin) \land \sum_{y \in x \cap A} ({F ↾}_{A}) (y) = \sum_{y \in x \cap A} ({F ↾}_{A}) (y)) \to \exists z \in (𝒫 A \cap Fin) \sum_{y \in x \cap A} ({F ↾}_{A}) (y) = \sum_{y \in z} ({F ↾}_{A}) (y)$
207	203 204 206	syl2anc	$⊢ x \in (𝒫 U \cap Fin) \to \exists z \in (𝒫 A \cap Fin) \sum_{y \in x \cap A} ({F ↾}_{A}) (y) = \sum_{y \in z} ({F ↾}_{A}) (y)$
208		sumex	$⊢ \sum_{y \in x \cap A} ({F ↾}_{A}) (y) \in V$
209	208	a1i	$⊢ x \in (𝒫 U \cap Fin) \to \sum_{y \in x \cap A} ({F ↾}_{A}) (y) \in V$
210	192 207 209	elrnmptd	$⊢ x \in (𝒫 U \cap Fin) \to \sum_{y \in x \cap A} ({F ↾}_{A}) (y) \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y))$
211	190 210	eqeltrd	$⊢ x \in (𝒫 U \cap Fin) \to \sum_{y \in x \cap A} F (y) \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y))$
212	211	3ad2ant2	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to \sum_{y \in x \cap A} F (y) \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y))$
213		sumeq1	$⊢ x = z \to \sum_{y \in x} ({F ↾}_{B}) (y) = \sum_{y \in z} ({F ↾}_{B}) (y)$
214	213	cbvmptv	$⊢ (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) = (z \in (𝒫 B \cap Fin) ⟼ \sum_{y \in z} ({F ↾}_{B}) (y))$
215		inss2	$⊢ x \cap B \subseteq B$
216	193	inex1	$⊢ x \cap B \in V$
217	216	elpw	$⊢ x \cap B \in 𝒫 B \leftrightarrow x \cap B \subseteq B$
218	215 217	mpbir	$⊢ x \cap B \in 𝒫 B$
219	218	a1i	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to x \cap B \in 𝒫 B$
220		inss1	$⊢ x \cap B \subseteq x$
221	220	a1i	$⊢ x \in (𝒫 U \cap Fin) \to x \cap B \subseteq x$
222		ssfi	$⊢ (x \in Fin \land x \cap B \subseteq x) \to x \cap B \in Fin$
223	198 221 222	syl2anc	$⊢ x \in (𝒫 U \cap Fin) \to x \cap B \in Fin$
224	223	3ad2ant2	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to x \cap B \in Fin$
225	219 224	elind	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to x \cap B \in (𝒫 B \cap Fin)$
226	215	sseli	$⊢ y \in (x \cap B) \to y \in B$
227	124	eqcomd	$⊢ y \in B \to F (y) = ({F ↾}_{B}) (y)$
228	226 227	syl	$⊢ y \in (x \cap B) \to F (y) = ({F ↾}_{B}) (y)$
229	228	sumeq2i	$⊢ \sum_{y \in x \cap B} F (y) = \sum_{y \in x \cap B} ({F ↾}_{B}) (y)$
230	229	a1i	$⊢ (φ \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x \cap B} F (y) = \sum_{y \in x \cap B} ({F ↾}_{B}) (y)$
231	230	3adant3	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to \sum_{y \in x \cap B} F (y) = \sum_{y \in x \cap B} ({F ↾}_{B}) (y)$
232		sumeq1	$⊢ z = x \cap B \to \sum_{y \in z} ({F ↾}_{B}) (y) = \sum_{y \in x \cap B} ({F ↾}_{B}) (y)$
233	232	rspceeqv	$⊢ (x \cap B \in (𝒫 B \cap Fin) \land \sum_{y \in x \cap B} F (y) = \sum_{y \in x \cap B} ({F ↾}_{B}) (y)) \to \exists z \in (𝒫 B \cap Fin) \sum_{y \in x \cap B} F (y) = \sum_{y \in z} ({F ↾}_{B}) (y)$
234	225 231 233	syl2anc	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to \exists z \in (𝒫 B \cap Fin) \sum_{y \in x \cap B} F (y) = \sum_{y \in z} ({F ↾}_{B}) (y)$
235		sumex	$⊢ \sum_{y \in x \cap B} F (y) \in V$
236	235	a1i	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to \sum_{y \in x \cap B} F (y) \in V$
237	214 234 236	elrnmptd	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to \sum_{y \in x \cap B} F (y) \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))$
238		simp3	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to r = \sum_{y \in x} F (y)$
239	185	a1i	$⊢ φ \to x \cap A \subseteq A$
240	215	a1i	$⊢ φ \to x \cap B \subseteq B$
241		ssin0	$⊢ (A \cap B = \emptyset \land x \cap A \subseteq A \land x \cap B \subseteq B) \to (x \cap A) \cap (x \cap B) = \emptyset$
242	4 239 240 241	syl3anc	$⊢ φ \to (x \cap A) \cap (x \cap B) = \emptyset$
243	242	adantr	$⊢ (φ \land x \in (𝒫 U \cap Fin)) \to (x \cap A) \cap (x \cap B) = \emptyset$
244		elinel1	$⊢ x \in (𝒫 U \cap Fin) \to x \in 𝒫 U$
245		elpwi	$⊢ x \in 𝒫 U \to x \subseteq U$
246	244 245	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \subseteq U$
247	3	ineq2i	$⊢ x \cap U = x \cap (A \cup B)$
248	247	a1i	$⊢ x \subseteq U \to x \cap U = x \cap (A \cup B)$
249		dfss	$⊢ x \subseteq U \leftrightarrow x = x \cap U$
250	249	biimpi	$⊢ x \subseteq U \to x = x \cap U$
251		indi	$⊢ x \cap (A \cup B) = (x \cap A) \cup (x \cap B)$
252	251	eqcomi	$⊢ (x \cap A) \cup (x \cap B) = x \cap (A \cup B)$
253	252	a1i	$⊢ x \subseteq U \to (x \cap A) \cup (x \cap B) = x \cap (A \cup B)$
254	248 250 253	3eqtr4d	$⊢ x \subseteq U \to x = (x \cap A) \cup (x \cap B)$
255	246 254	syl	$⊢ x \in (𝒫 U \cap Fin) \to x = (x \cap A) \cup (x \cap B)$
256	255	adantl	$⊢ (φ \land x \in (𝒫 U \cap Fin)) \to x = (x \cap A) \cup (x \cap B)$
257	198	adantl	$⊢ (φ \land x \in (𝒫 U \cap Fin)) \to x \in Fin$
258	144	ad2antrr	$⊢ ((φ \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F : U ⟶ [0, +∞)$
259	246	sselda	$⊢ (x \in (𝒫 U \cap Fin) \land y \in x) \to y \in U$
260	259	adantll	$⊢ ((φ \land x \in (𝒫 U \cap Fin)) \land y \in x) \to y \in U$
261	258 260	ffvelcdmd	$⊢ ((φ \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F (y) \in [0, +∞)$
262	143 261	sselid	$⊢ ((φ \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F (y) \in ℂ$
263	243 256 257 262	fsumsplit	$⊢ (φ \land x \in (𝒫 U \cap Fin)) \to \sum_{y \in x} F (y) = \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y)$
264	263	3adant3	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to \sum_{y \in x} F (y) = \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y)$
265	238 264	eqtrd	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to r = \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y)$
266		oveq2	$⊢ u = \sum_{y \in x \cap B} F (y) \to \sum_{y \in x \cap A} F (y) + u = \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y)$
267	266	rspceeqv	$⊢ (\sum_{y \in x \cap B} F (y) \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) \land r = \sum_{y \in x \cap A} F (y) + \sum_{y \in x \cap B} F (y)) \to \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = \sum_{y \in x \cap A} F (y) + u$
268	237 265 267	syl2anc	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = \sum_{y \in x \cap A} F (y) + u$
269		oveq1	$⊢ v = \sum_{y \in x \cap A} F (y) \to v + u = \sum_{y \in x \cap A} F (y) + u$
270	269	eqeq2d	$⊢ v = \sum_{y \in x \cap A} F (y) \to (r = v + u \leftrightarrow r = \sum_{y \in x \cap A} F (y) + u)$
271	270	rexbidv	$⊢ v = \sum_{y \in x \cap A} F (y) \to (\exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u \leftrightarrow \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = \sum_{y \in x \cap A} F (y) + u)$
272	271	rspcev	$⊢ (\sum_{y \in x \cap A} F (y) \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \land \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = \sum_{y \in x \cap A} F (y) + u) \to \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
273	212 268 272	syl2anc	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
274	273	3exp	$⊢ φ \to (x \in (𝒫 U \cap Fin) \to (r = \sum_{y \in x} F (y) \to \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u))$
275	274	adantr	$⊢ (φ \land r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))) \to (x \in (𝒫 U \cap Fin) \to (r = \sum_{y \in x} F (y) \to \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u))$
276	177 184 275	rexlimd	$⊢ (φ \land r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))) \to (\exists x \in (𝒫 U \cap Fin) r = \sum_{y \in x} F (y) \to \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u)$
277	171 276	mpd	$⊢ (φ \land r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))) \to \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
278	277 60	sylibr	$⊢ (φ \land r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))) \to r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\}$
279	278	ex	$⊢ φ \to (r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \to r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\})$
280	168 279	impbid	$⊢ φ \to (r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} \leftrightarrow r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
281	280	alrimiv	$⊢ φ \to \forall r (r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} \leftrightarrow r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
282		dfcleq	$⊢ \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} = ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) \leftrightarrow \forall r (r \in \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} \leftrightarrow r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
283	281 282	sylibr	$⊢ φ \to \{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} = ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
284	283	supeq1d	$⊢ φ \to sup (\{z \| \exists v \in ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) z = v + u\} ℝ <) = sup (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
285	27 54 284	3eqtrrd	$⊢ φ \to sup (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) +_{𝑒} sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <)$
286	15 5 6	sge0supre	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
287	17 24	oveq12d	$⊢ φ \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y)) ℝ <) +_{𝑒} sup (ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) ℝ <)$
288	285 286 287	3eqtr4d	$⊢ φ \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
289		rexadd	$⊢ (sum^({F ↾}_{A}) \in ℝ \land sum^({F ↾}_{B}) \in ℝ) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$
290	16 23 289	syl2anc	$⊢ φ \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$
291	288 290	eqtrd	$⊢ φ \to sum^(F) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$

Metamath Proof Explorer

Theorem sge0resplit

Proof