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