meadjiunlem

Description: The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meadjiunlem.f	$⊢ φ \to M \in Meas$
	meadjiunlem.3	$⊢ S = dom M$
	meadjiunlem.x	$⊢ φ \to X \in V$
	meadjiunlem.g	$⊢ φ \to G : X ⟶ S$
	meadjiunlem.y	$⊢ Y = \{i \in X \| G (i) \neq \emptyset\}$
	meadjiunlem.dj	$⊢ φ \to \underset{i \in X}{Disj} G (i)$
Assertion	meadjiunlem	$⊢ φ \to sum^({M ↾}_{ran G}) = sum^(M \circ G)$

Proof

Step	Hyp	Ref	Expression
1		meadjiunlem.f	$⊢ φ \to M \in Meas$
2		meadjiunlem.3	$⊢ S = dom M$
3		meadjiunlem.x	$⊢ φ \to X \in V$
4		meadjiunlem.g	$⊢ φ \to G : X ⟶ S$
5		meadjiunlem.y	$⊢ Y = \{i \in X \| G (i) \neq \emptyset\}$
6		meadjiunlem.dj	$⊢ φ \to \underset{i \in X}{Disj} G (i)$
7		nfv	$⊢ Ⅎ k φ$
8	4 3	jca	$⊢ φ \to (G : X ⟶ S \land X \in V)$
9		fex	$⊢ (G : X ⟶ S \land X \in V) \to G \in V$
10		rnexg	$⊢ G \in V \to ran G \in V$
11	8 9 10	3syl	$⊢ φ \to ran G \in V$
12		difssd	$⊢ φ \to ran G ∖ \{\emptyset\} \subseteq ran G$
13	1 2	meaf	$⊢ φ \to M : S ⟶ [0, +∞]$
14	13	adantr	$⊢ (φ \land k \in (ran G ∖ \{\emptyset\})) \to M : S ⟶ [0, +∞]$
15	4	frnd	$⊢ φ \to ran G \subseteq S$
16	15	adantr	$⊢ (φ \land k \in (ran G ∖ \{\emptyset\})) \to ran G \subseteq S$
17	12	sselda	$⊢ (φ \land k \in (ran G ∖ \{\emptyset\})) \to k \in ran G$
18	16 17	sseldd	$⊢ (φ \land k \in (ran G ∖ \{\emptyset\})) \to k \in S$
19	14 18	ffvelcdmd	$⊢ (φ \land k \in (ran G ∖ \{\emptyset\})) \to M (k) \in [0, +∞]$
20		simpl	$⊢ (φ \land k \in (ran G ∖ (ran G ∖ \{\emptyset\}))) \to φ$
21		id	$⊢ k \in (ran G ∖ (ran G ∖ \{\emptyset\})) \to k \in (ran G ∖ (ran G ∖ \{\emptyset\}))$
22		dfin4	$⊢ ran G \cap \{\emptyset\} = ran G ∖ (ran G ∖ \{\emptyset\})$
23	22	eqcomi	$⊢ ran G ∖ (ran G ∖ \{\emptyset\}) = ran G \cap \{\emptyset\}$
24	21 23	eleqtrdi	$⊢ k \in (ran G ∖ (ran G ∖ \{\emptyset\})) \to k \in (ran G \cap \{\emptyset\})$
25		elinel2	$⊢ k \in (ran G \cap \{\emptyset\}) \to k \in \{\emptyset\}$
26		elsni	$⊢ k \in \{\emptyset\} \to k = \emptyset$
27	25 26	syl	$⊢ k \in (ran G \cap \{\emptyset\}) \to k = \emptyset$
28	24 27	syl	$⊢ k \in (ran G ∖ (ran G ∖ \{\emptyset\})) \to k = \emptyset$
29	28	adantl	$⊢ (φ \land k \in (ran G ∖ (ran G ∖ \{\emptyset\}))) \to k = \emptyset$
30		simpr	$⊢ (φ \land k = \emptyset) \to k = \emptyset$
31	30	fveq2d	$⊢ (φ \land k = \emptyset) \to M (k) = M (\emptyset)$
32	1	mea0	$⊢ φ \to M (\emptyset) = 0$
33	32	adantr	$⊢ (φ \land k = \emptyset) \to M (\emptyset) = 0$
34	31 33	eqtrd	$⊢ (φ \land k = \emptyset) \to M (k) = 0$
35	20 29 34	syl2anc	$⊢ (φ \land k \in (ran G ∖ (ran G ∖ \{\emptyset\}))) \to M (k) = 0$
36	7 11 12 19 35	sge0ss	$⊢ φ \to sum^((k \in (ran G ∖ \{\emptyset\}) ⟼ M (k))) = sum^((k \in ran G ⟼ M (k)))$
37	36	eqcomd	$⊢ φ \to sum^((k \in ran G ⟼ M (k))) = sum^((k \in (ran G ∖ \{\emptyset\}) ⟼ M (k)))$
38	13 15	feqresmpt	$⊢ φ \to {M ↾}_{ran G} = (k \in ran G ⟼ M (k))$
39	38	fveq2d	$⊢ φ \to sum^({M ↾}_{ran G}) = sum^((k \in ran G ⟼ M (k)))$
40	4	ffvelcdmda	$⊢ (φ \land j \in X) \to G (j) \in S$
41	4	feqmptd	$⊢ φ \to G = (j \in X ⟼ G (j))$
42	13	feqmptd	$⊢ φ \to M = (k \in S ⟼ M (k))$
43		fveq2	$⊢ k = G (j) \to M (k) = M (G (j))$
44	40 41 42 43	fmptco	$⊢ φ \to M \circ G = (j \in X ⟼ M (G (j)))$
45	44	fveq2d	$⊢ φ \to sum^(M \circ G) = sum^((j \in X ⟼ M (G (j))))$
46		nfv	$⊢ Ⅎ j φ$
47		ssrab2	$⊢ \{i \in X \| G (i) \neq \emptyset\} \subseteq X$
48	47	a1i	$⊢ φ \to \{i \in X \| G (i) \neq \emptyset\} \subseteq X$
49	5 48	eqsstrid	$⊢ φ \to Y \subseteq X$
50	13	adantr	$⊢ (φ \land j \in Y) \to M : S ⟶ [0, +∞]$
51	4	adantr	$⊢ (φ \land j \in Y) \to G : X ⟶ S$
52	49	sselda	$⊢ (φ \land j \in Y) \to j \in X$
53	51 52	ffvelcdmd	$⊢ (φ \land j \in Y) \to G (j) \in S$
54	50 53	ffvelcdmd	$⊢ (φ \land j \in Y) \to M (G (j)) \in [0, +∞]$
55		eldifi	$⊢ j \in (X ∖ Y) \to j \in X$
56	55	ad2antlr	$⊢ ((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \to j \in X$
57		fveq2	$⊢ G (j) = \emptyset \to M (G (j)) = M (\emptyset)$
58	57	adantl	$⊢ (φ \land G (j) = \emptyset) \to M (G (j)) = M (\emptyset)$
59	1	adantr	$⊢ (φ \land G (j) = \emptyset) \to M \in Meas$
60	59	mea0	$⊢ (φ \land G (j) = \emptyset) \to M (\emptyset) = 0$
61	58 60	eqtrd	$⊢ (φ \land G (j) = \emptyset) \to M (G (j)) = 0$
62	61	ad4ant14	$⊢ (((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \land G (j) = \emptyset) \to M (G (j)) = 0$
63		neneq	$⊢ M (G (j)) \neq 0 \to \neg M (G (j)) = 0$
64	63	ad2antlr	$⊢ (((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \land G (j) = \emptyset) \to \neg M (G (j)) = 0$
65	62 64	pm2.65da	$⊢ ((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \to \neg G (j) = \emptyset$
66	65	neqned	$⊢ ((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \to G (j) \neq \emptyset$
67	56 66	jca	$⊢ ((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \to (j \in X \land G (j) \neq \emptyset)$
68		fveq2	$⊢ i = j \to G (i) = G (j)$
69	68	neeq1d	$⊢ i = j \to (G (i) \neq \emptyset \leftrightarrow G (j) \neq \emptyset)$
70	69	elrab	$⊢ j \in \{i \in X \| G (i) \neq \emptyset\} \leftrightarrow (j \in X \land G (j) \neq \emptyset)$
71	67 70	sylibr	$⊢ ((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \to j \in \{i \in X \| G (i) \neq \emptyset\}$
72	71 5	eleqtrrdi	$⊢ ((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \to j \in Y$
73		eldifn	$⊢ j \in (X ∖ Y) \to \neg j \in Y$
74	73	ad2antlr	$⊢ ((φ \land j \in (X ∖ Y)) \land M (G (j)) \neq 0) \to \neg j \in Y$
75	72 74	pm2.65da	$⊢ (φ \land j \in (X ∖ Y)) \to \neg M (G (j)) \neq 0$
76		nne	$⊢ \neg M (G (j)) \neq 0 \leftrightarrow M (G (j)) = 0$
77	75 76	sylib	$⊢ (φ \land j \in (X ∖ Y)) \to M (G (j)) = 0$
78	46 3 49 54 77	sge0ss	$⊢ φ \to sum^((j \in Y ⟼ M (G (j)))) = sum^((j \in X ⟼ M (G (j))))$
79	78	eqcomd	$⊢ φ \to sum^((j \in X ⟼ M (G (j)))) = sum^((j \in Y ⟼ M (G (j))))$
80	3 49	ssexd	$⊢ φ \to Y \in V$
81		nfv	$⊢ Ⅎ i φ$
82		eqid	$⊢ (i \in Y ⟼ G (i)) = (i \in Y ⟼ G (i))$
83	4	ffnd	$⊢ φ \to G Fn X$
84		dffn3	$⊢ G Fn X \leftrightarrow G : X ⟶ ran G$
85	83 84	sylib	$⊢ φ \to G : X ⟶ ran G$
86	85	adantr	$⊢ (φ \land i \in Y) \to G : X ⟶ ran G$
87	49	sselda	$⊢ (φ \land i \in Y) \to i \in X$
88	86 87	ffvelcdmd	$⊢ (φ \land i \in Y) \to G (i) \in ran G$
89	5	eleq2i	$⊢ i \in Y \leftrightarrow i \in \{i \in X \| G (i) \neq \emptyset\}$
90		rabid	$⊢ i \in \{i \in X \| G (i) \neq \emptyset\} \leftrightarrow (i \in X \land G (i) \neq \emptyset)$
91	89 90	bitri	$⊢ i \in Y \leftrightarrow (i \in X \land G (i) \neq \emptyset)$
92	91	biimpi	$⊢ i \in Y \to (i \in X \land G (i) \neq \emptyset)$
93	92	simprd	$⊢ i \in Y \to G (i) \neq \emptyset$
94	93	adantl	$⊢ (φ \land i \in Y) \to G (i) \neq \emptyset$
95		nelsn	$⊢ G (i) \neq \emptyset \to \neg G (i) \in \{\emptyset\}$
96	94 95	syl	$⊢ (φ \land i \in Y) \to \neg G (i) \in \{\emptyset\}$
97	88 96	eldifd	$⊢ (φ \land i \in Y) \to G (i) \in (ran G ∖ \{\emptyset\})$
98		disjss1	$⊢ Y \subseteq X \to (\underset{i \in X}{Disj} G (i) \to \underset{i \in Y}{Disj} G (i))$
99	49 6 98	sylc	$⊢ φ \to \underset{i \in Y}{Disj} G (i)$
100	81 82 97 94 99	disjf1	$⊢ φ \to (i \in Y ⟼ G (i)) : Y \underset{1-1}{⟶} ran G ∖ \{\emptyset\}$
101	4 49	feqresmpt	$⊢ φ \to {G ↾}_{Y} = (i \in Y ⟼ G (i))$
102		f1eq1	$⊢ {G ↾}_{Y} = (i \in Y ⟼ G (i)) \to (({G ↾}_{Y}) : Y \underset{1-1}{⟶} ran G ∖ \{\emptyset\} \leftrightarrow (i \in Y ⟼ G (i)) : Y \underset{1-1}{⟶} ran G ∖ \{\emptyset\})$
103	101 102	syl	$⊢ φ \to (({G ↾}_{Y}) : Y \underset{1-1}{⟶} ran G ∖ \{\emptyset\} \leftrightarrow (i \in Y ⟼ G (i)) : Y \underset{1-1}{⟶} ran G ∖ \{\emptyset\})$
104	100 103	mpbird	$⊢ φ \to ({G ↾}_{Y}) : Y \underset{1-1}{⟶} ran G ∖ \{\emptyset\}$
105	101	rneqd	$⊢ φ \to ran ({G ↾}_{Y}) = ran (i \in Y ⟼ G (i))$
106	97	ralrimiva	$⊢ φ \to \forall i \in Y G (i) \in (ran G ∖ \{\emptyset\})$
107	82	rnmptss	$⊢ \forall i \in Y G (i) \in (ran G ∖ \{\emptyset\}) \to ran (i \in Y ⟼ G (i)) \subseteq ran G ∖ \{\emptyset\}$
108	106 107	syl	$⊢ φ \to ran (i \in Y ⟼ G (i)) \subseteq ran G ∖ \{\emptyset\}$
109	105 108	eqsstrd	$⊢ φ \to ran ({G ↾}_{Y}) \subseteq ran G ∖ \{\emptyset\}$
110		simpl	$⊢ (φ \land x \in (ran G ∖ \{\emptyset\})) \to φ$
111		eldifi	$⊢ x \in (ran G ∖ \{\emptyset\}) \to x \in ran G$
112	111	adantl	$⊢ (φ \land x \in (ran G ∖ \{\emptyset\})) \to x \in ran G$
113		eldifsni	$⊢ x \in (ran G ∖ \{\emptyset\}) \to x \neq \emptyset$
114	113	adantl	$⊢ (φ \land x \in (ran G ∖ \{\emptyset\})) \to x \neq \emptyset$
115		simpr	$⊢ (φ \land x \in ran G) \to x \in ran G$
116		fvelrnb	$⊢ G Fn X \to (x \in ran G \leftrightarrow \exists i \in X G (i) = x)$
117	83 116	syl	$⊢ φ \to (x \in ran G \leftrightarrow \exists i \in X G (i) = x)$
118	117	adantr	$⊢ (φ \land x \in ran G) \to (x \in ran G \leftrightarrow \exists i \in X G (i) = x)$
119	115 118	mpbid	$⊢ (φ \land x \in ran G) \to \exists i \in X G (i) = x$
120	119	3adant3	$⊢ (φ \land x \in ran G \land x \neq \emptyset) \to \exists i \in X G (i) = x$
121		id	$⊢ G (i) = x \to G (i) = x$
122	121	eqcomd	$⊢ G (i) = x \to x = G (i)$
123	122	3ad2ant3	$⊢ ((φ \land x \neq \emptyset) \land i \in X \land G (i) = x) \to x = G (i)$
124		simp1l	$⊢ ((φ \land x \neq \emptyset) \land i \in X \land G (i) = x) \to φ$
125		simp2	$⊢ ((φ \land x \neq \emptyset) \land i \in X \land G (i) = x) \to i \in X$
126		simpr	$⊢ (x \neq \emptyset \land G (i) = x) \to G (i) = x$
127		simpl	$⊢ (x \neq \emptyset \land G (i) = x) \to x \neq \emptyset$
128	126 127	eqnetrd	$⊢ (x \neq \emptyset \land G (i) = x) \to G (i) \neq \emptyset$
129	128	adantll	$⊢ ((φ \land x \neq \emptyset) \land G (i) = x) \to G (i) \neq \emptyset$
130	129	3adant2	$⊢ ((φ \land x \neq \emptyset) \land i \in X \land G (i) = x) \to G (i) \neq \emptyset$
131	91	biimpri	$⊢ (i \in X \land G (i) \neq \emptyset) \to i \in Y$
132		fvexd	$⊢ (i \in X \land G (i) \neq \emptyset) \to G (i) \in V$
133	82	elrnmpt1	$⊢ (i \in Y \land G (i) \in V) \to G (i) \in ran (i \in Y ⟼ G (i))$
134	131 132 133	syl2anc	$⊢ (i \in X \land G (i) \neq \emptyset) \to G (i) \in ran (i \in Y ⟼ G (i))$
135	134	3adant1	$⊢ (φ \land i \in X \land G (i) \neq \emptyset) \to G (i) \in ran (i \in Y ⟼ G (i))$
136	105	eqcomd	$⊢ φ \to ran (i \in Y ⟼ G (i)) = ran ({G ↾}_{Y})$
137	136	3ad2ant1	$⊢ (φ \land i \in X \land G (i) \neq \emptyset) \to ran (i \in Y ⟼ G (i)) = ran ({G ↾}_{Y})$
138	135 137	eleqtrd	$⊢ (φ \land i \in X \land G (i) \neq \emptyset) \to G (i) \in ran ({G ↾}_{Y})$
139	124 125 130 138	syl3anc	$⊢ ((φ \land x \neq \emptyset) \land i \in X \land G (i) = x) \to G (i) \in ran ({G ↾}_{Y})$
140	123 139	eqeltrd	$⊢ ((φ \land x \neq \emptyset) \land i \in X \land G (i) = x) \to x \in ran ({G ↾}_{Y})$
141	140	3exp	$⊢ (φ \land x \neq \emptyset) \to (i \in X \to (G (i) = x \to x \in ran ({G ↾}_{Y})))$
142	141	rexlimdv	$⊢ (φ \land x \neq \emptyset) \to (\exists i \in X G (i) = x \to x \in ran ({G ↾}_{Y}))$
143	142	3adant2	$⊢ (φ \land x \in ran G \land x \neq \emptyset) \to (\exists i \in X G (i) = x \to x \in ran ({G ↾}_{Y}))$
144	120 143	mpd	$⊢ (φ \land x \in ran G \land x \neq \emptyset) \to x \in ran ({G ↾}_{Y})$
145	110 112 114 144	syl3anc	$⊢ (φ \land x \in (ran G ∖ \{\emptyset\})) \to x \in ran ({G ↾}_{Y})$
146	109 145	eqelssd	$⊢ φ \to ran ({G ↾}_{Y}) = ran G ∖ \{\emptyset\}$
147	104 146	jca	$⊢ φ \to (({G ↾}_{Y}) : Y \underset{1-1}{⟶} ran G ∖ \{\emptyset\} \land ran ({G ↾}_{Y}) = ran G ∖ \{\emptyset\})$
148		dff1o5	$⊢ ({G ↾}_{Y}) : Y \underset{1-1 onto}{⟶} ran G ∖ \{\emptyset\} \leftrightarrow (({G ↾}_{Y}) : Y \underset{1-1}{⟶} ran G ∖ \{\emptyset\} \land ran ({G ↾}_{Y}) = ran G ∖ \{\emptyset\})$
149	147 148	sylibr	$⊢ φ \to ({G ↾}_{Y}) : Y \underset{1-1 onto}{⟶} ran G ∖ \{\emptyset\}$
150		fvres	$⊢ j \in Y \to ({G ↾}_{Y}) (j) = G (j)$
151	150	adantl	$⊢ (φ \land j \in Y) \to ({G ↾}_{Y}) (j) = G (j)$
152	7 46 43 80 149 151 19	sge0f1o	$⊢ φ \to sum^((k \in (ran G ∖ \{\emptyset\}) ⟼ M (k))) = sum^((j \in Y ⟼ M (G (j))))$
153	152	eqcomd	$⊢ φ \to sum^((j \in Y ⟼ M (G (j)))) = sum^((k \in (ran G ∖ \{\emptyset\}) ⟼ M (k)))$
154	45 79 153	3eqtrd	$⊢ φ \to sum^(M \circ G) = sum^((k \in (ran G ∖ \{\emptyset\}) ⟼ M (k)))$
155	37 39 154	3eqtr4d	$⊢ φ \to sum^({M ↾}_{ran G}) = sum^(M \circ G)$

Metamath Proof Explorer

Theorem meadjiunlem

Proof