sge0iunmptlemfi

Description: Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0iunmptlemfi.a	$⊢ φ \to A \in Fin$
	sge0iunmptlemfi.b	$⊢ (φ \land x \in A) \to B \in V$
	sge0iunmptlemfi.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
	sge0iunmptlemfi.c	$⊢ (φ \land x \in A \land k \in B) \to C \in [0, +∞]$
	sge0iunmptlemfi.re	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \in ℝ$
Assertion	sge0iunmptlemfi	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$

Proof

Step	Hyp	Ref	Expression
1		sge0iunmptlemfi.a	$⊢ φ \to A \in Fin$
2		sge0iunmptlemfi.b	$⊢ (φ \land x \in A) \to B \in V$
3		sge0iunmptlemfi.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
4		sge0iunmptlemfi.c	$⊢ (φ \land x \in A \land k \in B) \to C \in [0, +∞]$
5		sge0iunmptlemfi.re	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \in ℝ$
6		iuneq1	$⊢ y = \emptyset \to ⋃_{x \in y} B = ⋃_{x \in \emptyset} B$
7	6	mpteq1d	$⊢ y = \emptyset \to (k \in ⋃_{x \in y} B ⟼ C) = (k \in ⋃_{x \in \emptyset} B ⟼ C)$
8	7	fveq2d	$⊢ y = \emptyset \to sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((k \in ⋃_{x \in \emptyset} B ⟼ C))$
9		mpteq1	$⊢ y = \emptyset \to (x \in y ⟼ sum^((k \in B ⟼ C))) = (x \in \emptyset ⟼ sum^((k \in B ⟼ C)))$
10	9	fveq2d	$⊢ y = \emptyset \to sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) = sum^((x \in \emptyset ⟼ sum^((k \in B ⟼ C))))$
11	8 10	eqeq12d	$⊢ y = \emptyset \to (sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) \leftrightarrow sum^((k \in ⋃_{x \in \emptyset} B ⟼ C)) = sum^((x \in \emptyset ⟼ sum^((k \in B ⟼ C)))))$
12		iuneq1	$⊢ y = z \to ⋃_{x \in y} B = ⋃_{x \in z} B$
13	12	mpteq1d	$⊢ y = z \to (k \in ⋃_{x \in y} B ⟼ C) = (k \in ⋃_{x \in z} B ⟼ C)$
14	13	fveq2d	$⊢ y = z \to sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((k \in ⋃_{x \in z} B ⟼ C))$
15		mpteq1	$⊢ y = z \to (x \in y ⟼ sum^((k \in B ⟼ C))) = (x \in z ⟼ sum^((k \in B ⟼ C)))$
16	15	fveq2d	$⊢ y = z \to sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))$
17	14 16	eqeq12d	$⊢ y = z \to (sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) \leftrightarrow sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C)))))$
18		iuneq1	$⊢ y = z \cup \{w\} \to ⋃_{x \in y} B = ⋃_{x \in z \cup \{w\}} B$
19	18	mpteq1d	$⊢ y = z \cup \{w\} \to (k \in ⋃_{x \in y} B ⟼ C) = (k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)$
20	19	fveq2d	$⊢ y = z \cup \{w\} \to sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C))$
21		mpteq1	$⊢ y = z \cup \{w\} \to (x \in y ⟼ sum^((k \in B ⟼ C))) = (x \in (z \cup \{w\}) ⟼ sum^((k \in B ⟼ C)))$
22	21	fveq2d	$⊢ y = z \cup \{w\} \to sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) = sum^((x \in (z \cup \{w\}) ⟼ sum^((k \in B ⟼ C))))$
23	20 22	eqeq12d	$⊢ y = z \cup \{w\} \to (sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) \leftrightarrow sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)) = sum^((x \in (z \cup \{w\}) ⟼ sum^((k \in B ⟼ C)))))$
24		iuneq1	$⊢ y = A \to ⋃_{x \in y} B = ⋃_{x \in A} B$
25	24	mpteq1d	$⊢ y = A \to (k \in ⋃_{x \in y} B ⟼ C) = (k \in ⋃_{x \in A} B ⟼ C)$
26	25	fveq2d	$⊢ y = A \to sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((k \in ⋃_{x \in A} B ⟼ C))$
27		mpteq1	$⊢ y = A \to (x \in y ⟼ sum^((k \in B ⟼ C))) = (x \in A ⟼ sum^((k \in B ⟼ C)))$
28	27	fveq2d	$⊢ y = A \to sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
29	26 28	eqeq12d	$⊢ y = A \to (sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) \leftrightarrow sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C)))))$
30		0iun	$⊢ ⋃_{x \in \emptyset} B = \emptyset$
31		mpteq1	$⊢ ⋃_{x \in \emptyset} B = \emptyset \to (k \in ⋃_{x \in \emptyset} B ⟼ C) = (k \in \emptyset ⟼ C)$
32	30 31	ax-mp	$⊢ (k \in ⋃_{x \in \emptyset} B ⟼ C) = (k \in \emptyset ⟼ C)$
33		mpt0	$⊢ (k \in \emptyset ⟼ C) = \emptyset$
34	32 33	eqtri	$⊢ (k \in ⋃_{x \in \emptyset} B ⟼ C) = \emptyset$
35	34	fveq2i	$⊢ sum^((k \in ⋃_{x \in \emptyset} B ⟼ C)) = sum^(\emptyset)$
36		mpt0	$⊢ (x \in \emptyset ⟼ sum^((k \in B ⟼ C))) = \emptyset$
37	36	fveq2i	$⊢ sum^((x \in \emptyset ⟼ sum^((k \in B ⟼ C)))) = sum^(\emptyset)$
38	35 37	eqtr4i	$⊢ sum^((k \in ⋃_{x \in \emptyset} B ⟼ C)) = sum^((x \in \emptyset ⟼ sum^((k \in B ⟼ C))))$
39	38	a1i	$⊢ φ \to sum^((k \in ⋃_{x \in \emptyset} B ⟼ C)) = sum^((x \in \emptyset ⟼ sum^((k \in B ⟼ C))))$
40		nfv	$⊢ Ⅎ x (φ \land (z \subseteq A \land w \in (A ∖ z)))$
41		nfcv	$⊢ \underline{Ⅎ} x sum^$
42		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in \{w\}} B$
43		nfcv	$⊢ \underline{Ⅎ} x C$
44	42 43	nfmpt	$⊢ \underline{Ⅎ} x (k \in ⋃_{x \in \{w\}} B ⟼ C)$
45	41 44	nffv	$⊢ \underline{Ⅎ} x sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
46		simprl	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to z \subseteq A$
47	1	adantr	$⊢ (φ \land z \subseteq A) \to A \in Fin$
48		simpr	$⊢ (φ \land z \subseteq A) \to z \subseteq A$
49		ssfi	$⊢ (A \in Fin \land z \subseteq A) \to z \in Fin$
50	47 48 49	syl2anc	$⊢ (φ \land z \subseteq A) \to z \in Fin$
51	46 50	syldan	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to z \in Fin$
52		simprr	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to w \in (A ∖ z)$
53		eldifn	$⊢ w \in (A ∖ z) \to \neg w \in z$
54		disjsn	$⊢ z \cap \{w\} = \emptyset \leftrightarrow \neg w \in z$
55	53 54	sylibr	$⊢ w \in (A ∖ z) \to z \cap \{w\} = \emptyset$
56	55	adantl	$⊢ (z \subseteq A \land w \in (A ∖ z)) \to z \cap \{w\} = \emptyset$
57	56	adantl	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to z \cap \{w\} = \emptyset$
58	57 54	sylib	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \neg w \in z$
59		simpll	$⊢ ((φ \land z \subseteq A) \land x \in z) \to φ$
60		ssel2	$⊢ (z \subseteq A \land x \in z) \to x \in A$
61	60	adantll	$⊢ ((φ \land z \subseteq A) \land x \in z) \to x \in A$
62	59 61 5	syl2anc	$⊢ ((φ \land z \subseteq A) \land x \in z) \to sum^((k \in B ⟼ C)) \in ℝ$
63	62	recnd	$⊢ ((φ \land z \subseteq A) \land x \in z) \to sum^((k \in B ⟼ C)) \in ℂ$
64	63	adantlrr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land x \in z) \to sum^((k \in B ⟼ C)) \in ℂ$
65		csbeq1a	$⊢ x = w \to B = ⦋ w / x ⦌ B$
66		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ w / x ⦌ B$
67		vex	$⊢ w \in V$
68	66 67 65	iunxsnf	$⊢ ⋃_{x \in \{w\}} B = ⦋ w / x ⦌ B$
69	65 68	syl6eqr	$⊢ x = w \to B = ⋃_{x \in \{w\}} B$
70	69	mpteq1d	$⊢ x = w \to (k \in B ⟼ C) = (k \in ⋃_{x \in \{w\}} B ⟼ C)$
71	70	fveq2d	$⊢ x = w \to sum^((k \in B ⟼ C)) = sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
72	68	mpteq1i	$⊢ (k \in ⋃_{x \in \{w\}} B ⟼ C) = (k \in ⦋ w / x ⦌ B ⟼ C)$
73	72	a1i	$⊢ (φ \land w \in (A ∖ z)) \to (k \in ⋃_{x \in \{w\}} B ⟼ C) = (k \in ⦋ w / x ⦌ B ⟼ C)$
74	73	fveq2d	$⊢ (φ \land w \in (A ∖ z)) \to sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) = sum^((k \in ⦋ w / x ⦌ B ⟼ C))$
75		eldifi	$⊢ w \in (A ∖ z) \to w \in A$
76		nfv	$⊢ Ⅎ x (φ \land w \in A)$
77	66 43	nfmpt	$⊢ \underline{Ⅎ} x (k \in ⦋ w / x ⦌ B ⟼ C)$
78	41 77	nffv	$⊢ \underline{Ⅎ} x sum^((k \in ⦋ w / x ⦌ B ⟼ C))$
79		nfcv	$⊢ \underline{Ⅎ} x ℝ$
80	78 79	nfel	$⊢ Ⅎ x sum^((k \in ⦋ w / x ⦌ B ⟼ C)) \in ℝ$
81	76 80	nfim	$⊢ Ⅎ x ((φ \land w \in A) \to sum^((k \in ⦋ w / x ⦌ B ⟼ C)) \in ℝ)$
82		eleq1w	$⊢ x = w \to (x \in A \leftrightarrow w \in A)$
83	82	anbi2d	$⊢ x = w \to ((φ \land x \in A) \leftrightarrow (φ \land w \in A))$
84	70 72	syl6eq	$⊢ x = w \to (k \in B ⟼ C) = (k \in ⦋ w / x ⦌ B ⟼ C)$
85	84	fveq2d	$⊢ x = w \to sum^((k \in B ⟼ C)) = sum^((k \in ⦋ w / x ⦌ B ⟼ C))$
86	85	eleq1d	$⊢ x = w \to (sum^((k \in B ⟼ C)) \in ℝ \leftrightarrow sum^((k \in ⦋ w / x ⦌ B ⟼ C)) \in ℝ)$
87	83 86	imbi12d	$⊢ x = w \to (((φ \land x \in A) \to sum^((k \in B ⟼ C)) \in ℝ) \leftrightarrow ((φ \land w \in A) \to sum^((k \in ⦋ w / x ⦌ B ⟼ C)) \in ℝ))$
88	81 87 5	chvarfv	$⊢ (φ \land w \in A) \to sum^((k \in ⦋ w / x ⦌ B ⟼ C)) \in ℝ$
89	75 88	sylan2	$⊢ (φ \land w \in (A ∖ z)) \to sum^((k \in ⦋ w / x ⦌ B ⟼ C)) \in ℝ$
90	74 89	eqeltrd	$⊢ (φ \land w \in (A ∖ z)) \to sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) \in ℝ$
91	90	adantrl	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) \in ℝ$
92	91	recnd	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) \in ℂ$
93	40 45 51 52 58 64 71 92	fsumsplitsn	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \sum_{x \in z \cup \{w\}} sum^((k \in B ⟼ C)) = \sum_{x \in z} sum^((k \in B ⟼ C)) + sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
94	93	eqcomd	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \sum_{x \in z} sum^((k \in B ⟼ C)) + sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) = \sum_{x \in z \cup \{w\}} sum^((k \in B ⟼ C))$
95	94	adantr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to \sum_{x \in z} sum^((k \in B ⟼ C)) + sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) = \sum_{x \in z \cup \{w\}} sum^((k \in B ⟼ C))$
96		iunxun	$⊢ ⋃_{x \in z \cup \{w\}} B = ⋃_{x \in z} B \cup ⋃_{x \in \{w\}} B$
97	96	mpteq1i	$⊢ (k \in ⋃_{x \in z \cup \{w\}} B ⟼ C) = (k \in (⋃_{x \in z} B \cup ⋃_{x \in \{w\}} B) ⟼ C)$
98	97	fveq2i	$⊢ sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)) = sum^((k \in (⋃_{x \in z} B \cup ⋃_{x \in \{w\}} B) ⟼ C))$
99	98	a1i	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)) = sum^((k \in (⋃_{x \in z} B \cup ⋃_{x \in \{w\}} B) ⟼ C))$
100		nfv	$⊢ Ⅎ k (φ \land (z \subseteq A \land w \in (A ∖ z)))$
101	2	ralrimiva	$⊢ φ \to \forall x \in A B \in V$
102		iunexg	$⊢ (A \in Fin \land \forall x \in A B \in V) \to ⋃_{x \in A} B \in V$
103	1 101 102	syl2anc	$⊢ φ \to ⋃_{x \in A} B \in V$
104	103	adantr	$⊢ (φ \land z \subseteq A) \to ⋃_{x \in A} B \in V$
105		iunss1	$⊢ z \subseteq A \to ⋃_{x \in z} B \subseteq ⋃_{x \in A} B$
106	105	adantl	$⊢ (φ \land z \subseteq A) \to ⋃_{x \in z} B \subseteq ⋃_{x \in A} B$
107	104 106	ssexd	$⊢ (φ \land z \subseteq A) \to ⋃_{x \in z} B \in V$
108	107	adantrr	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to ⋃_{x \in z} B \in V$
109	103	adantr	$⊢ (φ \land w \in (A ∖ z)) \to ⋃_{x \in A} B \in V$
110		snssi	$⊢ w \in A \to \{w\} \subseteq A$
111	75 110	syl	$⊢ w \in (A ∖ z) \to \{w\} \subseteq A$
112		iunss1	$⊢ \{w\} \subseteq A \to ⋃_{x \in \{w\}} B \subseteq ⋃_{x \in A} B$
113	111 112	syl	$⊢ w \in (A ∖ z) \to ⋃_{x \in \{w\}} B \subseteq ⋃_{x \in A} B$
114	113	adantl	$⊢ (φ \land w \in (A ∖ z)) \to ⋃_{x \in \{w\}} B \subseteq ⋃_{x \in A} B$
115	109 114	ssexd	$⊢ (φ \land w \in (A ∖ z)) \to ⋃_{x \in \{w\}} B \in V$
116	115	adantrl	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to ⋃_{x \in \{w\}} B \in V$
117	3	adantr	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \underset{x \in A}{Disj} B$
118	111	ad2antll	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \{w\} \subseteq A$
119		disjiun	$⊢ (\underset{x \in A}{Disj} B \land (z \subseteq A \land \{w\} \subseteq A \land z \cap \{w\} = \emptyset)) \to ⋃_{x \in z} B \cap ⋃_{x \in \{w\}} B = \emptyset$
120	117 46 118 57 119	syl13anc	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to ⋃_{x \in z} B \cap ⋃_{x \in \{w\}} B = \emptyset$
121		eliun	$⊢ k \in ⋃_{x \in z} B \leftrightarrow \exists x \in z k \in B$
122	121	biimpi	$⊢ k \in ⋃_{x \in z} B \to \exists x \in z k \in B$
123	122	adantl	$⊢ ((φ \land z \subseteq A) \land k \in ⋃_{x \in z} B) \to \exists x \in z k \in B$
124		simp1l	$⊢ ((φ \land z \subseteq A) \land x \in z \land k \in B) \to φ$
125	61	3adant3	$⊢ ((φ \land z \subseteq A) \land x \in z \land k \in B) \to x \in A$
126		simp3	$⊢ ((φ \land z \subseteq A) \land x \in z \land k \in B) \to k \in B$
127	124 125 126 4	syl3anc	$⊢ ((φ \land z \subseteq A) \land x \in z \land k \in B) \to C \in [0, +∞]$
128	127	3exp	$⊢ (φ \land z \subseteq A) \to (x \in z \to (k \in B \to C \in [0, +∞]))$
129	128	rexlimdv	$⊢ (φ \land z \subseteq A) \to (\exists x \in z k \in B \to C \in [0, +∞])$
130	129	adantr	$⊢ ((φ \land z \subseteq A) \land k \in ⋃_{x \in z} B) \to (\exists x \in z k \in B \to C \in [0, +∞])$
131	123 130	mpd	$⊢ ((φ \land z \subseteq A) \land k \in ⋃_{x \in z} B) \to C \in [0, +∞]$
132	131	adantlrr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land k \in ⋃_{x \in z} B) \to C \in [0, +∞]$
133		eliun	$⊢ k \in ⋃_{x \in \{w\}} B \leftrightarrow \exists x \in \{w\} k \in B$
134	133	biimpi	$⊢ k \in ⋃_{x \in \{w\}} B \to \exists x \in \{w\} k \in B$
135	134	adantl	$⊢ ((φ \land w \in (A ∖ z)) \land k \in ⋃_{x \in \{w\}} B) \to \exists x \in \{w\} k \in B$
136		simp1l	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\} \land k \in B) \to φ$
137	111	sselda	$⊢ (w \in (A ∖ z) \land x \in \{w\}) \to x \in A$
138	137	adantll	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\}) \to x \in A$
139	138	3adant3	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\} \land k \in B) \to x \in A$
140		simp3	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\} \land k \in B) \to k \in B$
141	136 139 140 4	syl3anc	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\} \land k \in B) \to C \in [0, +∞]$
142	141	3exp	$⊢ (φ \land w \in (A ∖ z)) \to (x \in \{w\} \to (k \in B \to C \in [0, +∞]))$
143	142	rexlimdv	$⊢ (φ \land w \in (A ∖ z)) \to (\exists x \in \{w\} k \in B \to C \in [0, +∞])$
144	143	adantr	$⊢ ((φ \land w \in (A ∖ z)) \land k \in ⋃_{x \in \{w\}} B) \to (\exists x \in \{w\} k \in B \to C \in [0, +∞])$
145	135 144	mpd	$⊢ ((φ \land w \in (A ∖ z)) \land k \in ⋃_{x \in \{w\}} B) \to C \in [0, +∞]$
146	145	adantlrl	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land k \in ⋃_{x \in \{w\}} B) \to C \in [0, +∞]$
147	100 108 116 120 132 146	sge0splitmpt	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to sum^((k \in (⋃_{x \in z} B \cup ⋃_{x \in \{w\}} B) ⟼ C)) = sum^((k \in ⋃_{x \in z} B ⟼ C)) +_{𝑒} sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
148	99 147	eqtrd	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)) = sum^((k \in ⋃_{x \in z} B ⟼ C)) +_{𝑒} sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
149	148	adantr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)) = sum^((k \in ⋃_{x \in z} B ⟼ C)) +_{𝑒} sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
150		id	$⊢ sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C)))) \to sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))$
151	150	adantl	$⊢ ((φ \land z \subseteq A) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))$
152	4	3expa	$⊢ ((φ \land x \in A) \land k \in B) \to C \in [0, +∞]$
153		eqid	$⊢ (k \in B ⟼ C) = (k \in B ⟼ C)$
154	152 153	fmptd	$⊢ (φ \land x \in A) \to (k \in B ⟼ C) : B ⟶ [0, +∞]$
155	2 154	sge0ge0	$⊢ (φ \land x \in A) \to 0 \leq sum^((k \in B ⟼ C))$
156	5 155	jca	$⊢ (φ \land x \in A) \to (sum^((k \in B ⟼ C)) \in ℝ \land 0 \leq sum^((k \in B ⟼ C)))$
157		elrege0	$⊢ sum^((k \in B ⟼ C)) \in [0, +∞) \leftrightarrow (sum^((k \in B ⟼ C)) \in ℝ \land 0 \leq sum^((k \in B ⟼ C)))$
158	156 157	sylibr	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \in [0, +∞)$
159	59 61 158	syl2anc	$⊢ ((φ \land z \subseteq A) \land x \in z) \to sum^((k \in B ⟼ C)) \in [0, +∞)$
160		eqid	$⊢ (x \in z ⟼ sum^((k \in B ⟼ C))) = (x \in z ⟼ sum^((k \in B ⟼ C)))$
161	159 160	fmptd	$⊢ (φ \land z \subseteq A) \to (x \in z ⟼ sum^((k \in B ⟼ C))) : z ⟶ [0, +∞)$
162	50 161	sge0fsum	$⊢ (φ \land z \subseteq A) \to sum^((x \in z ⟼ sum^((k \in B ⟼ C)))) = \sum_{y \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (y)$
163	162	adantr	$⊢ ((φ \land z \subseteq A) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((x \in z ⟼ sum^((k \in B ⟼ C)))) = \sum_{y \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (y)$
164		fveq2	$⊢ y = x \to (x \in z ⟼ sum^((k \in B ⟼ C))) (y) = (x \in z ⟼ sum^((k \in B ⟼ C))) (x)$
165		nfcv	$⊢ \underline{Ⅎ} x z$
166		nfcv	$⊢ \underline{Ⅎ} y z$
167		nfmpt1	$⊢ \underline{Ⅎ} x (x \in z ⟼ sum^((k \in B ⟼ C)))$
168		nfcv	$⊢ \underline{Ⅎ} x y$
169	167 168	nffv	$⊢ \underline{Ⅎ} x (x \in z ⟼ sum^((k \in B ⟼ C))) (y)$
170		nfcv	$⊢ \underline{Ⅎ} y (x \in z ⟼ sum^((k \in B ⟼ C))) (x)$
171	164 165 166 169 170	cbvsum	$⊢ \sum_{y \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (y) = \sum_{x \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (x)$
172	171	a1i	$⊢ (φ \land z \subseteq A) \to \sum_{y \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (y) = \sum_{x \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (x)$
173		id	$⊢ x \in z \to x \in z$
174		fvexd	$⊢ x \in z \to sum^((k \in B ⟼ C)) \in V$
175	160	fvmpt2	$⊢ (x \in z \land sum^((k \in B ⟼ C)) \in V) \to (x \in z ⟼ sum^((k \in B ⟼ C))) (x) = sum^((k \in B ⟼ C))$
176	173 174 175	syl2anc	$⊢ x \in z \to (x \in z ⟼ sum^((k \in B ⟼ C))) (x) = sum^((k \in B ⟼ C))$
177	176	adantl	$⊢ ((φ \land z \subseteq A) \land x \in z) \to (x \in z ⟼ sum^((k \in B ⟼ C))) (x) = sum^((k \in B ⟼ C))$
178	177	ralrimiva	$⊢ (φ \land z \subseteq A) \to \forall x \in z (x \in z ⟼ sum^((k \in B ⟼ C))) (x) = sum^((k \in B ⟼ C))$
179	178	sumeq2d	$⊢ (φ \land z \subseteq A) \to \sum_{x \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (x) = \sum_{x \in z} sum^((k \in B ⟼ C))$
180	172 179	eqtrd	$⊢ (φ \land z \subseteq A) \to \sum_{y \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (y) = \sum_{x \in z} sum^((k \in B ⟼ C))$
181	180	adantr	$⊢ ((φ \land z \subseteq A) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to \sum_{y \in z} (x \in z ⟼ sum^((k \in B ⟼ C))) (y) = \sum_{x \in z} sum^((k \in B ⟼ C))$
182	151 163 181	3eqtrd	$⊢ ((φ \land z \subseteq A) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((k \in ⋃_{x \in z} B ⟼ C)) = \sum_{x \in z} sum^((k \in B ⟼ C))$
183	182	adantlrr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((k \in ⋃_{x \in z} B ⟼ C)) = \sum_{x \in z} sum^((k \in B ⟼ C))$
184	183	oveq1d	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((k \in ⋃_{x \in z} B ⟼ C)) +_{𝑒} sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) = \sum_{x \in z} sum^((k \in B ⟼ C)) +_{𝑒} sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
185	50 62	fsumrecl	$⊢ (φ \land z \subseteq A) \to \sum_{x \in z} sum^((k \in B ⟼ C)) \in ℝ$
186	185	adantrr	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \sum_{x \in z} sum^((k \in B ⟼ C)) \in ℝ$
187		rexadd	$⊢ (\sum_{x \in z} sum^((k \in B ⟼ C)) \in ℝ \land sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) \in ℝ) \to \sum_{x \in z} sum^((k \in B ⟼ C)) +_{𝑒} sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) = \sum_{x \in z} sum^((k \in B ⟼ C)) + sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
188	186 91 187	syl2anc	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \sum_{x \in z} sum^((k \in B ⟼ C)) +_{𝑒} sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) = \sum_{x \in z} sum^((k \in B ⟼ C)) + sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
189	188	adantr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to \sum_{x \in z} sum^((k \in B ⟼ C)) +_{𝑒} sum^((k \in ⋃_{x \in \{w\}} B ⟼ C)) = \sum_{x \in z} sum^((k \in B ⟼ C)) + sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
190	149 184 189	3eqtrd	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)) = \sum_{x \in z} sum^((k \in B ⟼ C)) + sum^((k \in ⋃_{x \in \{w\}} B ⟼ C))$
191		snfi	$⊢ \{w\} \in Fin$
192	191	a1i	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \{w\} \in Fin$
193		unfi	$⊢ (z \in Fin \land \{w\} \in Fin) \to z \cup \{w\} \in Fin$
194	51 192 193	syl2anc	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to z \cup \{w\} \in Fin$
195		simpll	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land x \in (z \cup \{w\})) \to φ$
196	60	ad4ant14	$⊢ (((z \subseteq A \land w \in (A ∖ z)) \land x \in (z \cup \{w\})) \land x \in z) \to x \in A$
197		simpll	$⊢ ((w \in (A ∖ z) \land x \in (z \cup \{w\})) \land \neg x \in z) \to w \in (A ∖ z)$
198		elunnel1	$⊢ (x \in (z \cup \{w\}) \land \neg x \in z) \to x \in \{w\}$
199		elsni	$⊢ x \in \{w\} \to x = w$
200	198 199	syl	$⊢ (x \in (z \cup \{w\}) \land \neg x \in z) \to x = w$
201	200	adantll	$⊢ ((w \in (A ∖ z) \land x \in (z \cup \{w\})) \land \neg x \in z) \to x = w$
202		simpr	$⊢ (w \in (A ∖ z) \land x = w) \to x = w$
203	75	adantr	$⊢ (w \in (A ∖ z) \land x = w) \to w \in A$
204	202 203	eqeltrd	$⊢ (w \in (A ∖ z) \land x = w) \to x \in A$
205	197 201 204	syl2anc	$⊢ ((w \in (A ∖ z) \land x \in (z \cup \{w\})) \land \neg x \in z) \to x \in A$
206	205	adantlll	$⊢ (((z \subseteq A \land w \in (A ∖ z)) \land x \in (z \cup \{w\})) \land \neg x \in z) \to x \in A$
207	196 206	pm2.61dan	$⊢ ((z \subseteq A \land w \in (A ∖ z)) \land x \in (z \cup \{w\})) \to x \in A$
208	207	adantll	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land x \in (z \cup \{w\})) \to x \in A$
209	195 208 158	syl2anc	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land x \in (z \cup \{w\})) \to sum^((k \in B ⟼ C)) \in [0, +∞)$
210	194 209	sge0fsummpt	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to sum^((x \in (z \cup \{w\}) ⟼ sum^((k \in B ⟼ C)))) = \sum_{x \in z \cup \{w\}} sum^((k \in B ⟼ C))$
211	210	adantr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((x \in (z \cup \{w\}) ⟼ sum^((k \in B ⟼ C)))) = \sum_{x \in z \cup \{w\}} sum^((k \in B ⟼ C))$
212	95 190 211	3eqtr4d	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C))))) \to sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)) = sum^((x \in (z \cup \{w\}) ⟼ sum^((k \in B ⟼ C))))$
213	212	ex	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to (sum^((k \in ⋃_{x \in z} B ⟼ C)) = sum^((x \in z ⟼ sum^((k \in B ⟼ C)))) \to sum^((k \in ⋃_{x \in z \cup \{w\}} B ⟼ C)) = sum^((x \in (z \cup \{w\}) ⟼ sum^((k \in B ⟼ C)))))$
214	11 17 23 29 39 213 1	findcard2d	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$

Metamath Proof Explorer

Theorem sge0iunmptlemfi

Proof