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	eqtr4di	$⊢ 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	eqtrdi	$⊢ 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	bilani	$⊢ ((φ \land z \subseteq A) \land k \in ⋃_{x \in z} B) \to \exists x \in z k \in B$
123		simp1l	$⊢ ((φ \land z \subseteq A) \land x \in z \land k \in B) \to φ$
124	61	3adant3	$⊢ ((φ \land z \subseteq A) \land x \in z \land k \in B) \to x \in A$
125		simp3	$⊢ ((φ \land z \subseteq A) \land x \in z \land k \in B) \to k \in B$
126	123 124 125 4	syl3anc	$⊢ ((φ \land z \subseteq A) \land x \in z \land k \in B) \to C \in [0, +∞]$
127	126	3exp	$⊢ (φ \land z \subseteq A) \to (x \in z \to (k \in B \to C \in [0, +∞]))$
128	127	rexlimdv	$⊢ (φ \land z \subseteq A) \to (\exists x \in z k \in B \to C \in [0, +∞])$
129	128	adantr	$⊢ ((φ \land z \subseteq A) \land k \in ⋃_{x \in z} B) \to (\exists x \in z k \in B \to C \in [0, +∞])$
130	122 129	mpd	$⊢ ((φ \land z \subseteq A) \land k \in ⋃_{x \in z} B) \to C \in [0, +∞]$
131	130	adantlrr	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land k \in ⋃_{x \in z} B) \to C \in [0, +∞]$
132		eliun	$⊢ k \in ⋃_{x \in \{w\}} B \leftrightarrow \exists x \in \{w\} k \in B$
133	132	bilani	$⊢ ((φ \land w \in (A ∖ z)) \land k \in ⋃_{x \in \{w\}} B) \to \exists x \in \{w\} k \in B$
134		simp1l	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\} \land k \in B) \to φ$
135	111	sselda	$⊢ (w \in (A ∖ z) \land x \in \{w\}) \to x \in A$
136	135	adantll	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\}) \to x \in A$
137	136	3adant3	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\} \land k \in B) \to x \in A$
138		simp3	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\} \land k \in B) \to k \in B$
139	134 137 138 4	syl3anc	$⊢ ((φ \land w \in (A ∖ z)) \land x \in \{w\} \land k \in B) \to C \in [0, +∞]$
140	139	3exp	$⊢ (φ \land w \in (A ∖ z)) \to (x \in \{w\} \to (k \in B \to C \in [0, +∞]))$
141	140	rexlimdv	$⊢ (φ \land w \in (A ∖ z)) \to (\exists x \in \{w\} k \in B \to C \in [0, +∞])$
142	141	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, +∞])$
143	133 142	mpd	$⊢ ((φ \land w \in (A ∖ z)) \land k \in ⋃_{x \in \{w\}} B) \to C \in [0, +∞]$
144	143	adantlrl	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land k \in ⋃_{x \in \{w\}} B) \to C \in [0, +∞]$
145	100 108 116 120 131 144	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))$
146	99 145	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))$
147	146	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))$
148		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))))$
149	148	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))))$
150	4	3expa	$⊢ ((φ \land x \in A) \land k \in B) \to C \in [0, +∞]$
151		eqid	$⊢ (k \in B ⟼ C) = (k \in B ⟼ C)$
152	150 151	fmptd	$⊢ (φ \land x \in A) \to (k \in B ⟼ C) : B ⟶ [0, +∞]$
153	2 152	sge0ge0	$⊢ (φ \land x \in A) \to 0 \leq sum^((k \in B ⟼ C))$
154	5 153	jca	$⊢ (φ \land x \in A) \to (sum^((k \in B ⟼ C)) \in ℝ \land 0 \leq sum^((k \in B ⟼ C)))$
155		elrege0	$⊢ sum^((k \in B ⟼ C)) \in [0, +∞) \leftrightarrow (sum^((k \in B ⟼ C)) \in ℝ \land 0 \leq sum^((k \in B ⟼ C)))$
156	154 155	sylibr	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \in [0, +∞)$
157	59 61 156	syl2anc	$⊢ ((φ \land z \subseteq A) \land x \in z) \to sum^((k \in B ⟼ C)) \in [0, +∞)$
158		eqid	$⊢ (x \in z ⟼ sum^((k \in B ⟼ C))) = (x \in z ⟼ sum^((k \in B ⟼ C)))$
159	157 158	fmptd	$⊢ (φ \land z \subseteq A) \to (x \in z ⟼ sum^((k \in B ⟼ C))) : z ⟶ [0, +∞)$
160	50 159	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)$
161	160	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)$
162		fveq2	$⊢ y = x \to (x \in z ⟼ sum^((k \in B ⟼ C))) (y) = (x \in z ⟼ sum^((k \in B ⟼ C))) (x)$
163		nfmpt1	$⊢ \underline{Ⅎ} x (x \in z ⟼ sum^((k \in B ⟼ C)))$
164		nfcv	$⊢ \underline{Ⅎ} x y$
165	163 164	nffv	$⊢ \underline{Ⅎ} x (x \in z ⟼ sum^((k \in B ⟼ C))) (y)$
166		nfcv	$⊢ \underline{Ⅎ} y (x \in z ⟼ sum^((k \in B ⟼ C))) (x)$
167	162 165 166	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)$
168	167	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)$
169		id	$⊢ x \in z \to x \in z$
170		fvexd	$⊢ x \in z \to sum^((k \in B ⟼ C)) \in V$
171	158	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))$
172	169 170 171	syl2anc	$⊢ x \in z \to (x \in z ⟼ sum^((k \in B ⟼ C))) (x) = sum^((k \in B ⟼ C))$
173	172	adantl	$⊢ ((φ \land z \subseteq A) \land x \in z) \to (x \in z ⟼ sum^((k \in B ⟼ C))) (x) = sum^((k \in B ⟼ C))$
174	173	ralrimiva	$⊢ (φ \land z \subseteq A) \to \forall x \in z (x \in z ⟼ sum^((k \in B ⟼ C))) (x) = sum^((k \in B ⟼ C))$
175	174	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))$
176	168 175	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))$
177	176	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))$
178	149 161 177	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))$
179	178	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))$
180	179	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))$
181	50 62	fsumrecl	$⊢ (φ \land z \subseteq A) \to \sum_{x \in z} sum^((k \in B ⟼ C)) \in ℝ$
182	181	adantrr	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \sum_{x \in z} sum^((k \in B ⟼ C)) \in ℝ$
183		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))$
184	182 91 183	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))$
185	184	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))$
186	147 180 185	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))$
187		snfi	$⊢ \{w\} \in Fin$
188	187	a1i	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to \{w\} \in Fin$
189		unfi	$⊢ (z \in Fin \land \{w\} \in Fin) \to z \cup \{w\} \in Fin$
190	51 188 189	syl2anc	$⊢ (φ \land (z \subseteq A \land w \in (A ∖ z))) \to z \cup \{w\} \in Fin$
191		simpll	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land x \in (z \cup \{w\})) \to φ$
192	60	ad4ant14	$⊢ (((z \subseteq A \land w \in (A ∖ z)) \land x \in (z \cup \{w\})) \land x \in z) \to x \in A$
193		simpll	$⊢ ((w \in (A ∖ z) \land x \in (z \cup \{w\})) \land \neg x \in z) \to w \in (A ∖ z)$
194		elunnel1	$⊢ (x \in (z \cup \{w\}) \land \neg x \in z) \to x \in \{w\}$
195		elsni	$⊢ x \in \{w\} \to x = w$
196	194 195	syl	$⊢ (x \in (z \cup \{w\}) \land \neg x \in z) \to x = w$
197	196	adantll	$⊢ ((w \in (A ∖ z) \land x \in (z \cup \{w\})) \land \neg x \in z) \to x = w$
198		simpr	$⊢ (w \in (A ∖ z) \land x = w) \to x = w$
199	75	adantr	$⊢ (w \in (A ∖ z) \land x = w) \to w \in A$
200	198 199	eqeltrd	$⊢ (w \in (A ∖ z) \land x = w) \to x \in A$
201	193 197 200	syl2anc	$⊢ ((w \in (A ∖ z) \land x \in (z \cup \{w\})) \land \neg x \in z) \to x \in A$
202	201	adantlll	$⊢ (((z \subseteq A \land w \in (A ∖ z)) \land x \in (z \cup \{w\})) \land \neg x \in z) \to x \in A$
203	192 202	pm2.61dan	$⊢ ((z \subseteq A \land w \in (A ∖ z)) \land x \in (z \cup \{w\})) \to x \in A$
204	203	adantll	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land x \in (z \cup \{w\})) \to x \in A$
205	191 204 156	syl2anc	$⊢ ((φ \land (z \subseteq A \land w \in (A ∖ z))) \land x \in (z \cup \{w\})) \to sum^((k \in B ⟼ C)) \in [0, +∞)$
206	190 205	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))$
207	206	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))$
208	95 186 207	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))))$
209	208	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)))))$
210	11 17 23 29 39 209 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