sge0iunmpt

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		sge0iunmpt.a	$⊢ φ \to A \in V$
2		sge0iunmpt.b	$⊢ (φ \land x \in A) \to B \in W$
3		sge0iunmpt.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
4		sge0iunmpt.c	$⊢ (φ \land x \in A \land k \in B) \to C \in [0, +∞]$
5		nfv	$⊢ Ⅎ x φ$
6		nfcv	$⊢ \underline{Ⅎ} x sum^$
7		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} B$
8		nfcv	$⊢ \underline{Ⅎ} x C$
9	7 8	nfmpt	$⊢ \underline{Ⅎ} x (k \in ⋃_{x \in A} B ⟼ C)$
10	6 9	nffv	$⊢ \underline{Ⅎ} x sum^((k \in ⋃_{x \in A} B ⟼ C))$
11		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ sum^((k \in B ⟼ C)))$
12	6 11	nffv	$⊢ \underline{Ⅎ} x sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
13	10 12	nfeq	$⊢ Ⅎ x sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
14	2	ralrimiva	$⊢ φ \to \forall x \in A B \in W$
15		iunexg	$⊢ (A \in V \land \forall x \in A B \in W) \to ⋃_{x \in A} B \in V$
16	1 14 15	syl2anc	$⊢ φ \to ⋃_{x \in A} B \in V$
17		eliun	$⊢ k \in ⋃_{x \in A} B \leftrightarrow \exists x \in A k \in B$
18	17	biimpi	$⊢ k \in ⋃_{x \in A} B \to \exists x \in A k \in B$
19	18	adantl	$⊢ (φ \land k \in ⋃_{x \in A} B) \to \exists x \in A k \in B$
20		nfcv	$⊢ \underline{Ⅎ} x k$
21	20 7	nfel	$⊢ Ⅎ x k \in ⋃_{x \in A} B$
22	5 21	nfan	$⊢ Ⅎ x (φ \land k \in ⋃_{x \in A} B)$
23	8	nfel1	$⊢ Ⅎ x C \in [0, +∞]$
24	4	3exp	$⊢ φ \to (x \in A \to (k \in B \to C \in [0, +∞]))$
25	24	adantr	$⊢ (φ \land k \in ⋃_{x \in A} B) \to (x \in A \to (k \in B \to C \in [0, +∞]))$
26	22 23 25	rexlimd	$⊢ (φ \land k \in ⋃_{x \in A} B) \to (\exists x \in A k \in B \to C \in [0, +∞])$
27	19 26	mpd	$⊢ (φ \land k \in ⋃_{x \in A} B) \to C \in [0, +∞]$
28		eqid	$⊢ (k \in ⋃_{x \in A} B ⟼ C) = (k \in ⋃_{x \in A} B ⟼ C)$
29	27 28	fmptd	$⊢ φ \to (k \in ⋃_{x \in A} B ⟼ C) : ⋃_{x \in A} B ⟶ [0, +∞]$
30	16 29	sge0xrcl	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) \in ℝ^{*}$
31	30	3ad2ant1	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to sum^((k \in ⋃_{x \in A} B ⟼ C)) \in ℝ^{*}$
32		id	$⊢ sum^((k \in B ⟼ C)) = +∞ \to sum^((k \in B ⟼ C)) = +∞$
33	32	eqcomd	$⊢ sum^((k \in B ⟼ C)) = +∞ \to +∞ = sum^((k \in B ⟼ C))$
34	33	adantl	$⊢ (x \in A \land sum^((k \in B ⟼ C)) = +∞) \to +∞ = sum^((k \in B ⟼ C))$
35	34	3adant1	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to +∞ = sum^((k \in B ⟼ C))$
36	16	adantr	$⊢ (φ \land x \in A) \to ⋃_{x \in A} B \in V$
37	27	adantlr	$⊢ ((φ \land x \in A) \land k \in ⋃_{x \in A} B) \to C \in [0, +∞]$
38		ssiun2	$⊢ x \in A \to B \subseteq ⋃_{x \in A} B$
39	38	adantl	$⊢ (φ \land x \in A) \to B \subseteq ⋃_{x \in A} B$
40	36 37 39	sge0lessmpt	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \leq sum^((k \in ⋃_{x \in A} B ⟼ C))$
41	40	3adant3	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to sum^((k \in B ⟼ C)) \leq sum^((k \in ⋃_{x \in A} B ⟼ C))$
42	35 41	eqbrtrd	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to +∞ \leq sum^((k \in ⋃_{x \in A} B ⟼ C))$
43	31 42	xrgepnfd	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = +∞$
44	1	3ad2ant1	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to A \in V$
45		nfv	$⊢ Ⅎ x (φ \land y \in A)$
46		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
47		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ W$
48	46 47	nfel	$⊢ Ⅎ x ⦋ y / x ⦌ B \in ⦋ y / x ⦌ W$
49	45 48	nfim	$⊢ Ⅎ x ((φ \land y \in A) \to ⦋ y / x ⦌ B \in ⦋ y / x ⦌ W)$
50		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
51	50	anbi2d	$⊢ x = y \to ((φ \land x \in A) \leftrightarrow (φ \land y \in A))$
52		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
53		csbeq1a	$⊢ x = y \to W = ⦋ y / x ⦌ W$
54	52 53	eleq12d	$⊢ x = y \to (B \in W \leftrightarrow ⦋ y / x ⦌ B \in ⦋ y / x ⦌ W)$
55	51 54	imbi12d	$⊢ x = y \to (((φ \land x \in A) \to B \in W) \leftrightarrow ((φ \land y \in A) \to ⦋ y / x ⦌ B \in ⦋ y / x ⦌ W))$
56	49 55 2	chvarfv	$⊢ (φ \land y \in A) \to ⦋ y / x ⦌ B \in ⦋ y / x ⦌ W$
57	56	adantlr	$⊢ ((φ \land x \in A) \land y \in A) \to ⦋ y / x ⦌ B \in ⦋ y / x ⦌ W$
58	46 8	nfmpt	$⊢ \underline{Ⅎ} x (k \in ⦋ y / x ⦌ B ⟼ C)$
59		nfcv	$⊢ \underline{Ⅎ} x [0, +∞]$
60	58 46 59	nff	$⊢ Ⅎ x (k \in ⦋ y / x ⦌ B ⟼ C) : ⦋ y / x ⦌ B ⟶ [0, +∞]$
61	45 60	nfim	$⊢ Ⅎ x ((φ \land y \in A) \to (k \in ⦋ y / x ⦌ B ⟼ C) : ⦋ y / x ⦌ B ⟶ [0, +∞])$
62	52	mpteq1d	$⊢ x = y \to (k \in B ⟼ C) = (k \in ⦋ y / x ⦌ B ⟼ C)$
63	62 52	feq12d	$⊢ x = y \to ((k \in B ⟼ C) : B ⟶ [0, +∞] \leftrightarrow (k \in ⦋ y / x ⦌ B ⟼ C) : ⦋ y / x ⦌ B ⟶ [0, +∞])$
64	51 63	imbi12d	$⊢ x = y \to (((φ \land x \in A) \to (k \in B ⟼ C) : B ⟶ [0, +∞]) \leftrightarrow ((φ \land y \in A) \to (k \in ⦋ y / x ⦌ B ⟼ C) : ⦋ y / x ⦌ B ⟶ [0, +∞]))$
65	24	imp31	$⊢ ((φ \land x \in A) \land k \in B) \to C \in [0, +∞]$
66		eqid	$⊢ (k \in B ⟼ C) = (k \in B ⟼ C)$
67	65 66	fmptd	$⊢ (φ \land x \in A) \to (k \in B ⟼ C) : B ⟶ [0, +∞]$
68	61 64 67	chvarfv	$⊢ (φ \land y \in A) \to (k \in ⦋ y / x ⦌ B ⟼ C) : ⦋ y / x ⦌ B ⟶ [0, +∞]$
69	68	adantlr	$⊢ ((φ \land x \in A) \land y \in A) \to (k \in ⦋ y / x ⦌ B ⟼ C) : ⦋ y / x ⦌ B ⟶ [0, +∞]$
70	57 69	sge0cl	$⊢ ((φ \land x \in A) \land y \in A) \to sum^((k \in ⦋ y / x ⦌ B ⟼ C)) \in [0, +∞]$
71		nfcv	$⊢ \underline{Ⅎ} y sum^((k \in B ⟼ C))$
72	6 58	nffv	$⊢ \underline{Ⅎ} x sum^((k \in ⦋ y / x ⦌ B ⟼ C))$
73	62	fveq2d	$⊢ x = y \to sum^((k \in B ⟼ C)) = sum^((k \in ⦋ y / x ⦌ B ⟼ C))$
74	71 72 73	cbvmpt	$⊢ (x \in A ⟼ sum^((k \in B ⟼ C))) = (y \in A ⟼ sum^((k \in ⦋ y / x ⦌ B ⟼ C)))$
75	70 74	fmptd	$⊢ (φ \land x \in A) \to (x \in A ⟼ sum^((k \in B ⟼ C))) : A ⟶ [0, +∞]$
76	75	3adant3	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to (x \in A ⟼ sum^((k \in B ⟼ C))) : A ⟶ [0, +∞]$
77		id	$⊢ x \in A \to x \in A$
78		fvexd	$⊢ x \in A \to sum^((k \in B ⟼ C)) \in V$
79		eqid	$⊢ (x \in A ⟼ sum^((k \in B ⟼ C))) = (x \in A ⟼ sum^((k \in B ⟼ C)))$
80	79	elrnmpt1	$⊢ (x \in A \land sum^((k \in B ⟼ C)) \in V) \to sum^((k \in B ⟼ C)) \in ran (x \in A ⟼ sum^((k \in B ⟼ C)))$
81	77 78 80	syl2anc	$⊢ x \in A \to sum^((k \in B ⟼ C)) \in ran (x \in A ⟼ sum^((k \in B ⟼ C)))$
82	81	adantr	$⊢ (x \in A \land sum^((k \in B ⟼ C)) = +∞) \to sum^((k \in B ⟼ C)) \in ran (x \in A ⟼ sum^((k \in B ⟼ C)))$
83	34 82	eqeltrd	$⊢ (x \in A \land sum^((k \in B ⟼ C)) = +∞) \to +∞ \in ran (x \in A ⟼ sum^((k \in B ⟼ C)))$
84	83	3adant1	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to +∞ \in ran (x \in A ⟼ sum^((k \in B ⟼ C)))$
85	44 76 84	sge0pnfval	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) = +∞$
86	43 85	eqtr4d	$⊢ (φ \land x \in A \land sum^((k \in B ⟼ C)) = +∞) \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
87	86	3exp	$⊢ φ \to (x \in A \to (sum^((k \in B ⟼ C)) = +∞ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))))$
88	5 13 87	rexlimd	$⊢ φ \to (\exists x \in A sum^((k \in B ⟼ C)) = +∞ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C)))))$
89	88	imp	$⊢ (φ \land \exists x \in A sum^((k \in B ⟼ C)) = +∞) \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
90		simpl	$⊢ (φ \land \neg \exists x \in A sum^((k \in B ⟼ C)) = +∞) \to φ$
91		ralnex	$⊢ \forall x \in A \neg sum^((k \in B ⟼ C)) = +∞ \leftrightarrow \neg \exists x \in A sum^((k \in B ⟼ C)) = +∞$
92		df-ne	$⊢ sum^((k \in B ⟼ C)) \neq +∞ \leftrightarrow \neg sum^((k \in B ⟼ C)) = +∞$
93	92	bicomi	$⊢ \neg sum^((k \in B ⟼ C)) = +∞ \leftrightarrow sum^((k \in B ⟼ C)) \neq +∞$
94	93	ralbii	$⊢ \forall x \in A \neg sum^((k \in B ⟼ C)) = +∞ \leftrightarrow \forall x \in A sum^((k \in B ⟼ C)) \neq +∞$
95	91 94	sylbb1	$⊢ \neg \exists x \in A sum^((k \in B ⟼ C)) = +∞ \to \forall x \in A sum^((k \in B ⟼ C)) \neq +∞$
96	95	adantl	$⊢ (φ \land \neg \exists x \in A sum^((k \in B ⟼ C)) = +∞) \to \forall x \in A sum^((k \in B ⟼ C)) \neq +∞$
97	1	adantr	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to A \in V$
98		nfcv	$⊢ \underline{Ⅎ} x W$
99	46 98	nfel	$⊢ Ⅎ x ⦋ y / x ⦌ B \in W$
100	45 99	nfim	$⊢ Ⅎ x ((φ \land y \in A) \to ⦋ y / x ⦌ B \in W)$
101	52	eleq1d	$⊢ x = y \to (B \in W \leftrightarrow ⦋ y / x ⦌ B \in W)$
102	51 101	imbi12d	$⊢ x = y \to (((φ \land x \in A) \to B \in W) \leftrightarrow ((φ \land y \in A) \to ⦋ y / x ⦌ B \in W))$
103	100 102 2	chvarfv	$⊢ (φ \land y \in A) \to ⦋ y / x ⦌ B \in W$
104	103	adantlr	$⊢ ((φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \land y \in A) \to ⦋ y / x ⦌ B \in W$
105		nfcv	$⊢ \underline{Ⅎ} y B$
106	105 46 52	cbvdisj	$⊢ \underset{x \in A}{Disj} B \leftrightarrow \underset{y \in A}{Disj} ⦋ y / x ⦌ B$
107	3 106	sylib	$⊢ φ \to \underset{y \in A}{Disj} ⦋ y / x ⦌ B$
108	107	adantr	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to \underset{y \in A}{Disj} ⦋ y / x ⦌ B$
109		nfv	$⊢ Ⅎ k (φ \land y \in A \land j \in ⦋ y / x ⦌ B)$
110		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ C$
111	110	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ C \in [0, +∞]$
112	109 111	nfim	$⊢ Ⅎ k ((φ \land y \in A \land j \in ⦋ y / x ⦌ B) \to ⦋ j / k ⦌ C \in [0, +∞])$
113		eleq1w	$⊢ k = j \to (k \in ⦋ y / x ⦌ B \leftrightarrow j \in ⦋ y / x ⦌ B)$
114	113	3anbi3d	$⊢ k = j \to ((φ \land y \in A \land k \in ⦋ y / x ⦌ B) \leftrightarrow (φ \land y \in A \land j \in ⦋ y / x ⦌ B))$
115		csbeq1a	$⊢ k = j \to C = ⦋ j / k ⦌ C$
116	115	eleq1d	$⊢ k = j \to (C \in [0, +∞] \leftrightarrow ⦋ j / k ⦌ C \in [0, +∞])$
117	114 116	imbi12d	$⊢ k = j \to (((φ \land y \in A \land k \in ⦋ y / x ⦌ B) \to C \in [0, +∞]) \leftrightarrow ((φ \land y \in A \land j \in ⦋ y / x ⦌ B) \to ⦋ j / k ⦌ C \in [0, +∞]))$
118		nfv	$⊢ Ⅎ x y \in A$
119	20 46	nfel	$⊢ Ⅎ x k \in ⦋ y / x ⦌ B$
120	5 118 119	nf3an	$⊢ Ⅎ x (φ \land y \in A \land k \in ⦋ y / x ⦌ B)$
121	120 23	nfim	$⊢ Ⅎ x ((φ \land y \in A \land k \in ⦋ y / x ⦌ B) \to C \in [0, +∞])$
122	52	eleq2d	$⊢ x = y \to (k \in B \leftrightarrow k \in ⦋ y / x ⦌ B)$
123	50 122	3anbi23d	$⊢ x = y \to ((φ \land x \in A \land k \in B) \leftrightarrow (φ \land y \in A \land k \in ⦋ y / x ⦌ B))$
124	123	imbi1d	$⊢ x = y \to (((φ \land x \in A \land k \in B) \to C \in [0, +∞]) \leftrightarrow ((φ \land y \in A \land k \in ⦋ y / x ⦌ B) \to C \in [0, +∞]))$
125	121 124 4	chvarfv	$⊢ (φ \land y \in A \land k \in ⦋ y / x ⦌ B) \to C \in [0, +∞]$
126	112 117 125	chvarfv	$⊢ (φ \land y \in A \land j \in ⦋ y / x ⦌ B) \to ⦋ j / k ⦌ C \in [0, +∞]$
127	126	3adant1r	$⊢ ((φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \land y \in A \land j \in ⦋ y / x ⦌ B) \to ⦋ j / k ⦌ C \in [0, +∞]$
128		simpr	$⊢ (\forall x \in A sum^((k \in B ⟼ C)) \neq +∞ \land y \in A) \to y \in A$
129		simpl	$⊢ (\forall x \in A sum^((k \in B ⟼ C)) \neq +∞ \land y \in A) \to \forall x \in A sum^((k \in B ⟼ C)) \neq +∞$
130		simpl	$⊢ (y \in A \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to y \in A$
131		simpr	$⊢ (y \in A \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to \forall x \in A sum^((k \in B ⟼ C)) \neq +∞$
132		nfcv	$⊢ \underline{Ⅎ} x ⦋ j / k ⦌ C$
133	46 132	nfmpt	$⊢ \underline{Ⅎ} x (j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)$
134	6 133	nffv	$⊢ \underline{Ⅎ} x sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C))$
135		nfcv	$⊢ \underline{Ⅎ} x +∞$
136	134 135	nfne	$⊢ Ⅎ x sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \neq +∞$
137		nfcv	$⊢ \underline{Ⅎ} j C$
138	137 110 115	cbvmpt	$⊢ (k \in ⦋ y / x ⦌ B ⟼ C) = (j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)$
139	138	a1i	$⊢ x = y \to (k \in ⦋ y / x ⦌ B ⟼ C) = (j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)$
140	62 139	eqtrd	$⊢ x = y \to (k \in B ⟼ C) = (j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)$
141	140	fveq2d	$⊢ x = y \to sum^((k \in B ⟼ C)) = sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C))$
142	141	neeq1d	$⊢ x = y \to (sum^((k \in B ⟼ C)) \neq +∞ \leftrightarrow sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \neq +∞)$
143	136 142	rspc	$⊢ y \in A \to (\forall x \in A sum^((k \in B ⟼ C)) \neq +∞ \to sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \neq +∞)$
144	130 131 143	sylc	$⊢ (y \in A \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \neq +∞$
145	128 129 144	syl2anc	$⊢ (\forall x \in A sum^((k \in B ⟼ C)) \neq +∞ \land y \in A) \to sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \neq +∞$
146	145	neneqd	$⊢ (\forall x \in A sum^((k \in B ⟼ C)) \neq +∞ \land y \in A) \to \neg sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) = +∞$
147	146	adantll	$⊢ ((φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \land y \in A) \to \neg sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) = +∞$
148	126	3expa	$⊢ ((φ \land y \in A) \land j \in ⦋ y / x ⦌ B) \to ⦋ j / k ⦌ C \in [0, +∞]$
149		eqid	$⊢ (j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C) = (j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)$
150	148 149	fmptd	$⊢ (φ \land y \in A) \to (j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C) : ⦋ y / x ⦌ B ⟶ [0, +∞]$
151	150	adantlr	$⊢ ((φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \land y \in A) \to (j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C) : ⦋ y / x ⦌ B ⟶ [0, +∞]$
152	104 151	sge0repnf	$⊢ ((φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \land y \in A) \to (sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \in ℝ \leftrightarrow \neg sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) = +∞)$
153	147 152	mpbird	$⊢ ((φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \land y \in A) \to sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \in ℝ$
154	137 110 115	cbvmpt	$⊢ (k \in ⋃_{x \in A} B ⟼ C) = (j \in ⋃_{x \in A} B ⟼ ⦋ j / k ⦌ C)$
155	105 46 52	cbviun	$⊢ ⋃_{x \in A} B = ⋃_{y \in A} ⦋ y / x ⦌ B$
156	155	mpteq1i	$⊢ (j \in ⋃_{x \in A} B ⟼ ⦋ j / k ⦌ C) = (j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)$
157	154 156	eqtri	$⊢ (k \in ⋃_{x \in A} B ⟼ C) = (j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)$
158	157	fveq2i	$⊢ sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C))$
159	158 30	eqeltrrid	$⊢ φ \to sum^((j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \in ℝ^{*}$
160	159	adantr	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to sum^((j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) \in ℝ^{*}$
161	71 134 141	cbvmpt	$⊢ (x \in A ⟼ sum^((k \in B ⟼ C))) = (y \in A ⟼ sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)))$
162	161	fveq2i	$⊢ sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) = sum^((y \in A ⟼ sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C))))$
163	2 67	sge0cl	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \in [0, +∞]$
164	163 79	fmptd	$⊢ φ \to (x \in A ⟼ sum^((k \in B ⟼ C))) : A ⟶ [0, +∞]$
165	1 164	sge0xrcl	$⊢ φ \to sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) \in ℝ^{*}$
166	162 165	eqeltrrid	$⊢ φ \to sum^((y \in A ⟼ sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)))) \in ℝ^{*}$
167	166	adantr	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to sum^((y \in A ⟼ sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)))) \in ℝ^{*}$
168		eliun	$⊢ j \in ⋃_{y \in A} ⦋ y / x ⦌ B \leftrightarrow \exists y \in A j \in ⦋ y / x ⦌ B$
169	168	biimpi	$⊢ j \in ⋃_{y \in A} ⦋ y / x ⦌ B \to \exists y \in A j \in ⦋ y / x ⦌ B$
170	169	adantl	$⊢ (φ \land j \in ⋃_{y \in A} ⦋ y / x ⦌ B) \to \exists y \in A j \in ⦋ y / x ⦌ B$
171		nfv	$⊢ Ⅎ y φ$
172		nfcv	$⊢ \underline{Ⅎ} y j$
173		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in A} ⦋ y / x ⦌ B$
174	172 173	nfel	$⊢ Ⅎ y j \in ⋃_{y \in A} ⦋ y / x ⦌ B$
175	171 174	nfan	$⊢ Ⅎ y (φ \land j \in ⋃_{y \in A} ⦋ y / x ⦌ B)$
176		nfv	$⊢ Ⅎ y ⦋ j / k ⦌ C \in [0, +∞]$
177	148	exp31	$⊢ φ \to (y \in A \to (j \in ⦋ y / x ⦌ B \to ⦋ j / k ⦌ C \in [0, +∞]))$
178	177	adantr	$⊢ (φ \land j \in ⋃_{y \in A} ⦋ y / x ⦌ B) \to (y \in A \to (j \in ⦋ y / x ⦌ B \to ⦋ j / k ⦌ C \in [0, +∞]))$
179	175 176 178	rexlimd	$⊢ (φ \land j \in ⋃_{y \in A} ⦋ y / x ⦌ B) \to (\exists y \in A j \in ⦋ y / x ⦌ B \to ⦋ j / k ⦌ C \in [0, +∞])$
180	170 179	mpd	$⊢ (φ \land j \in ⋃_{y \in A} ⦋ y / x ⦌ B) \to ⦋ j / k ⦌ C \in [0, +∞]$
181		eqid	$⊢ (j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C) = (j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)$
182	180 181	fmptd	$⊢ φ \to (j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C) : ⋃_{y \in A} ⦋ y / x ⦌ B ⟶ [0, +∞]$
183	182	adantr	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to (j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C) : ⋃_{y \in A} ⦋ y / x ⦌ B ⟶ [0, +∞]$
184	155 16	eqeltrrid	$⊢ φ \to ⋃_{y \in A} ⦋ y / x ⦌ B \in V$
185	184	adantr	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to ⋃_{y \in A} ⦋ y / x ⦌ B \in V$
186	97 104 108 127 153 160 167 183 185	sge0iunmptlemre	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to sum^((j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C)) = sum^((y \in A ⟼ sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C))))$
187	158	a1i	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((j \in ⋃_{y \in A} ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C))$
188	162	a1i	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) = sum^((y \in A ⟼ sum^((j \in ⦋ y / x ⦌ B ⟼ ⦋ j / k ⦌ C))))$
189	186 187 188	3eqtr4d	$⊢ (φ \land \forall x \in A sum^((k \in B ⟼ C)) \neq +∞) \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
190	90 96 189	syl2anc	$⊢ (φ \land \neg \exists x \in A sum^((k \in B ⟼ C)) = +∞) \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
191	89 190	pm2.61dan	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$

Metamath Proof Explorer

Theorem sge0iunmpt

Proof