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	bilani	$⊢ (φ \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$
62		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 φ$
63		vex	$⊢ v \in V$
64		sumeq1	$⊢ x = a \to \sum_{y \in x} ({F ↾}_{A}) (y) = \sum_{y \in a} ({F ↾}_{A}) (y)$
65	64	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))$
66	65	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))$
67	63 66	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)$
68	67	birani	$⊢ (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)$
69		vex	$⊢ u \in V$
70		sumeq1	$⊢ x = b \to \sum_{y \in x} ({F ↾}_{B}) (y) = \sum_{y \in b} ({F ↾}_{B}) (y)$
71	70	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))$
72	71	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))$
73	69 72	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)$
74	73	bilani	$⊢ (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)$
75	68 74	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))$
76		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))$
77	75 76	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))$
78	77	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))$
79		eqid	$⊢ (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
80		elinel1	$⊢ a \in (𝒫 A \cap Fin) \to a \in 𝒫 A$
81		elpwi	$⊢ a \in 𝒫 A \to a \subseteq A$
82		id	$⊢ a \subseteq A \to a \subseteq A$
83	82 9	sstrdi	$⊢ a \subseteq A \to a \subseteq U$
84	81 83	syl	$⊢ a \in 𝒫 A \to a \subseteq U$
85	80 84	syl	$⊢ a \in (𝒫 A \cap Fin) \to a \subseteq U$
86	85	adantr	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \subseteq U$
87		elinel1	$⊢ b \in (𝒫 B \cap Fin) \to b \in 𝒫 B$
88		elpwi	$⊢ b \in 𝒫 B \to b \subseteq B$
89		id	$⊢ b \subseteq B \to b \subseteq B$
90	89 20	sstrdi	$⊢ b \subseteq B \to b \subseteq U$
91	88 90	syl	$⊢ b \in 𝒫 B \to b \subseteq U$
92	87 91	syl	$⊢ b \in (𝒫 B \cap Fin) \to b \subseteq U$
93	92	adantl	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to b \subseteq U$
94	86 93	unssd	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \cup b \subseteq U$
95		vex	$⊢ a \in V$
96		vex	$⊢ b \in V$
97	95 96	unex	$⊢ a \cup b \in V$
98	97	elpw	$⊢ a \cup b \in 𝒫 U \leftrightarrow a \cup b \subseteq U$
99	94 98	sylibr	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \cup b \in 𝒫 U$
100		elinel2	$⊢ a \in (𝒫 A \cap Fin) \to a \in Fin$
101	100	adantr	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \in Fin$
102		elinel2	$⊢ b \in (𝒫 B \cap Fin) \to b \in Fin$
103	102	adantl	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to b \in Fin$
104		unfi	$⊢ (a \in Fin \land b \in Fin) \to a \cup b \in Fin$
105	101 103 104	syl2anc	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \cup b \in Fin$
106	99 105	elind	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to a \cup b \in (𝒫 U \cap Fin)$
107	106	adantl	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \cup b \in (𝒫 U \cap Fin)$
108	107	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)$
109		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)$
110		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)$
111	109 110	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)$
112	111	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)$
113	80 81	syl	$⊢ a \in (𝒫 A \cap Fin) \to a \subseteq A$
114	113	sselda	$⊢ (a \in (𝒫 A \cap Fin) \land y \in a) \to y \in A$
115		fvres	$⊢ y \in A \to ({F ↾}_{A}) (y) = F (y)$
116	114 115	syl	$⊢ (a \in (𝒫 A \cap Fin) \land y \in a) \to ({F ↾}_{A}) (y) = F (y)$
117	116	sumeq2dv	$⊢ a \in (𝒫 A \cap Fin) \to \sum_{y \in a} ({F ↾}_{A}) (y) = \sum_{y \in a} F (y)$
118	117	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)$
119	87 88	syl	$⊢ b \in (𝒫 B \cap Fin) \to b \subseteq B$
120	119	sselda	$⊢ (b \in (𝒫 B \cap Fin) \land y \in b) \to y \in B$
121		fvres	$⊢ y \in B \to ({F ↾}_{B}) (y) = F (y)$
122	120 121	syl	$⊢ (b \in (𝒫 B \cap Fin) \land y \in b) \to ({F ↾}_{B}) (y) = F (y)$
123	122	sumeq2dv	$⊢ b \in (𝒫 B \cap Fin) \to \sum_{y \in b} ({F ↾}_{B}) (y) = \sum_{y \in b} F (y)$
124	123	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)$
125	118 124	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)$
126	125	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)$
127	112 126	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)$
128	127	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)$
129		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$
130	4	adantr	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to A \cap B = \emptyset$
131	113	ad2antrl	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \subseteq A$
132	119	adantl	$⊢ (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \to b \subseteq B$
133	132	adantl	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to b \subseteq B$
134		ssin0	$⊢ (A \cap B = \emptyset \land a \subseteq A \land b \subseteq B) \to a \cap b = \emptyset$
135	130 131 133 134	syl3anc	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \cap b = \emptyset$
136		eqidd	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \cup b = a \cup b$
137	105	adantl	$⊢ (φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \to a \cup b \in Fin$
138		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
139		ax-resscn	$⊢ ℝ \subseteq ℂ$
140	138 139	sstri	$⊢ [0, +∞) \subseteq ℂ$
141	5 28	fge0iccico	$⊢ φ \to F : U ⟶ [0, +∞)$
142	141	ad2antrr	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land y \in (a \cup b)) \to F : U ⟶ [0, +∞)$
143	94	sselda	$⊢ ((a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin)) \land y \in (a \cup b)) \to y \in U$
144	143	adantll	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land y \in (a \cup b)) \to y \in U$
145	142 144	ffvelcdmd	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land y \in (a \cup b)) \to F (y) \in [0, +∞)$
146	140 145	sselid	$⊢ ((φ \land (a \in (𝒫 A \cap Fin) \land b \in (𝒫 B \cap Fin))) \land y \in (a \cup b)) \to F (y) \in ℂ$
147	135 136 137 146	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)$
148	147	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)$
149	128 129 148	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)$
150		sumeq1	$⊢ x = a \cup b \to \sum_{y \in x} F (y) = \sum_{y \in a \cup b} F (y)$
151	150	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)$
152	108 149 151	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)$
153	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$
154	79 152 153	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))$
155	154	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)))$
156	155	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))))$
157	156	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)))))$
158	157	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))))$
159	158	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)))$
160	62 78 159	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)))$
161	160	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))))$
162	161	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)))$
163	162	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))$
164	55 61 163	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))$
165	164	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)))$
166	79	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))$
167	166	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)$
168	167	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)$
169		nfv	$⊢ Ⅎ x φ$
170		nfcv	$⊢ \underline{Ⅎ} x r$
171		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
172	171	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
173	170 172	nfel	$⊢ Ⅎ x r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y))$
174	169 173	nfan	$⊢ Ⅎ x (φ \land r \in ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)))$
175		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y))$
176	175	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{A}) (y))$
177		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))$
178	177	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y))$
179		nfv	$⊢ Ⅎ x r = v + u$
180	178 179	nfrexw	$⊢ Ⅎ x \exists u \in ran (x \in (𝒫 B \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{B}) (y)) r = v + u$
181	176 180	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$
182		inss2	$⊢ x \cap A \subseteq A$
183	182	sseli	$⊢ y \in (x \cap A) \to y \in A$
184	183	adantl	$⊢ (x \in (𝒫 U \cap Fin) \land y \in (x \cap A)) \to y \in A$
185	115	eqcomd	$⊢ y \in A \to F (y) = ({F ↾}_{A}) (y)$
186	184 185	syl	$⊢ (x \in (𝒫 U \cap Fin) \land y \in (x \cap A)) \to F (y) = ({F ↾}_{A}) (y)$
187	186	sumeq2dv	$⊢ x \in (𝒫 U \cap Fin) \to \sum_{y \in x \cap A} F (y) = \sum_{y \in x \cap A} ({F ↾}_{A}) (y)$
188		sumeq1	$⊢ x = z \to \sum_{y \in x} ({F ↾}_{A}) (y) = \sum_{y \in z} ({F ↾}_{A}) (y)$
189	188	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))$
190		vex	$⊢ x \in V$
191	190	inex1	$⊢ x \cap A \in V$
192	191	elpw	$⊢ x \cap A \in 𝒫 A \leftrightarrow x \cap A \subseteq A$
193	182 192	mpbir	$⊢ x \cap A \in 𝒫 A$
194	193	a1i	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \in 𝒫 A$
195		elinel2	$⊢ x \in (𝒫 U \cap Fin) \to x \in Fin$
196		inss1	$⊢ x \cap A \subseteq x$
197	196	a1i	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \subseteq x$
198		ssfi	$⊢ (x \in Fin \land x \cap A \subseteq x) \to x \cap A \in Fin$
199	195 197 198	syl2anc	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \in Fin$
200	194 199	elind	$⊢ x \in (𝒫 U \cap Fin) \to x \cap A \in (𝒫 A \cap Fin)$
201		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)$
202		sumeq1	$⊢ z = x \cap A \to \sum_{y \in z} ({F ↾}_{A}) (y) = \sum_{y \in x \cap A} ({F ↾}_{A}) (y)$
203	202	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)$
204	200 201 203	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)$
205		sumex	$⊢ \sum_{y \in x \cap A} ({F ↾}_{A}) (y) \in V$
206	205	a1i	$⊢ x \in (𝒫 U \cap Fin) \to \sum_{y \in x \cap A} ({F ↾}_{A}) (y) \in V$
207	189 204 206	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))$
208	187 207	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))$
209	208	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))$
210		sumeq1	$⊢ x = z \to \sum_{y \in x} ({F ↾}_{B}) (y) = \sum_{y \in z} ({F ↾}_{B}) (y)$
211	210	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))$
212		inss2	$⊢ x \cap B \subseteq B$
213	190	inex1	$⊢ x \cap B \in V$
214	213	elpw	$⊢ x \cap B \in 𝒫 B \leftrightarrow x \cap B \subseteq B$
215	212 214	mpbir	$⊢ x \cap B \in 𝒫 B$
216	215	a1i	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to x \cap B \in 𝒫 B$
217		inss1	$⊢ x \cap B \subseteq x$
218	217	a1i	$⊢ x \in (𝒫 U \cap Fin) \to x \cap B \subseteq x$
219		ssfi	$⊢ (x \in Fin \land x \cap B \subseteq x) \to x \cap B \in Fin$
220	195 218 219	syl2anc	$⊢ x \in (𝒫 U \cap Fin) \to x \cap B \in Fin$
221	220	3ad2ant2	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to x \cap B \in Fin$
222	216 221	elind	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to x \cap B \in (𝒫 B \cap Fin)$
223	212	sseli	$⊢ y \in (x \cap B) \to y \in B$
224	121	eqcomd	$⊢ y \in B \to F (y) = ({F ↾}_{B}) (y)$
225	223 224	syl	$⊢ y \in (x \cap B) \to F (y) = ({F ↾}_{B}) (y)$
226	225	sumeq2i	$⊢ \sum_{y \in x \cap B} F (y) = \sum_{y \in x \cap B} ({F ↾}_{B}) (y)$
227	226	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)$
228	227	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)$
229		sumeq1	$⊢ z = x \cap B \to \sum_{y \in z} ({F ↾}_{B}) (y) = \sum_{y \in x \cap B} ({F ↾}_{B}) (y)$
230	229	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)$
231	222 228 230	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)$
232		sumex	$⊢ \sum_{y \in x \cap B} F (y) \in V$
233	232	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$
234	211 231 233	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))$
235		simp3	$⊢ (φ \land x \in (𝒫 U \cap Fin) \land r = \sum_{y \in x} F (y)) \to r = \sum_{y \in x} F (y)$
236	182	a1i	$⊢ φ \to x \cap A \subseteq A$
237	212	a1i	$⊢ φ \to x \cap B \subseteq B$
238		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$
239	4 236 237 238	syl3anc	$⊢ φ \to (x \cap A) \cap (x \cap B) = \emptyset$
240	239	adantr	$⊢ (φ \land x \in (𝒫 U \cap Fin)) \to (x \cap A) \cap (x \cap B) = \emptyset$
241		elinel1	$⊢ x \in (𝒫 U \cap Fin) \to x \in 𝒫 U$
242		elpwi	$⊢ x \in 𝒫 U \to x \subseteq U$
243	241 242	syl	$⊢ x \in (𝒫 U \cap Fin) \to x \subseteq U$
244	3	ineq2i	$⊢ x \cap U = x \cap (A \cup B)$
245	244	a1i	$⊢ x \subseteq U \to x \cap U = x \cap (A \cup B)$
246		dfss	$⊢ x \subseteq U \leftrightarrow x = x \cap U$
247	246	biimpi	$⊢ x \subseteq U \to x = x \cap U$
248		indi	$⊢ x \cap (A \cup B) = (x \cap A) \cup (x \cap B)$
249	248	eqcomi	$⊢ (x \cap A) \cup (x \cap B) = x \cap (A \cup B)$
250	249	a1i	$⊢ x \subseteq U \to (x \cap A) \cup (x \cap B) = x \cap (A \cup B)$
251	245 247 250	3eqtr4d	$⊢ x \subseteq U \to x = (x \cap A) \cup (x \cap B)$
252	243 251	syl	$⊢ x \in (𝒫 U \cap Fin) \to x = (x \cap A) \cup (x \cap B)$
253	252	adantl	$⊢ (φ \land x \in (𝒫 U \cap Fin)) \to x = (x \cap A) \cup (x \cap B)$
254	195	adantl	$⊢ (φ \land x \in (𝒫 U \cap Fin)) \to x \in Fin$
255	141	ad2antrr	$⊢ ((φ \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F : U ⟶ [0, +∞)$
256	243	sselda	$⊢ (x \in (𝒫 U \cap Fin) \land y \in x) \to y \in U$
257	256	adantll	$⊢ ((φ \land x \in (𝒫 U \cap Fin)) \land y \in x) \to y \in U$
258	255 257	ffvelcdmd	$⊢ ((φ \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F (y) \in [0, +∞)$
259	140 258	sselid	$⊢ ((φ \land x \in (𝒫 U \cap Fin)) \land y \in x) \to F (y) \in ℂ$
260	240 253 254 259	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)$
261	260	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)$
262	235 261	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)$
263		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)$
264	263	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$
265	234 262 264	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$
266		oveq1	$⊢ v = \sum_{y \in x \cap A} F (y) \to v + u = \sum_{y \in x \cap A} F (y) + u$
267	266	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)$
268	267	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)$
269	268	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$
270	209 265 269	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$
271	270	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))$
272	271	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))$
273	174 181 272	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)$
274	168 273	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$
275	274 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\}$
276	275	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\})$
277	165 276	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)))$
278	277	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)))$
279		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)))$
280	278 279	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))$
281	280	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)) ℝ <)$
282	27 54 281	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)) ℝ <)$
283	15 5 6	sge0supre	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 U \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
284	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)) ℝ <)$
285	282 283 284	3eqtr4d	$⊢ φ \to sum^(F) = sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B})$
286		rexadd	$⊢ (sum^({F ↾}_{A}) \in ℝ \land sum^({F ↾}_{B}) \in ℝ) \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$
287	16 23 286	syl2anc	$⊢ φ \to sum^({F ↾}_{A}) +_{𝑒} sum^({F ↾}_{B}) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$
288	285 287	eqtrd	$⊢ φ \to sum^(F) = sum^({F ↾}_{A}) + sum^({F ↾}_{B})$

Metamath Proof Explorer

Theorem sge0resplit

Proof