psmeasurelem

Description: M applied to a disjoint union of subsets of its domain is the sum of M applied to such subset. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	psmeasurelem.x	$⊢ φ \to X \in V$
	psmeasurelem.h	$⊢ φ \to H : X ⟶ [0, +∞]$
	psmeasurelem.m	$⊢ M = (x \in 𝒫 X ⟼ sum^({H ↾}_{x}))$
	psmeasurelem.mf	$⊢ φ \to M : 𝒫 X ⟶ [0, +∞]$
	psmeasurelem.y	$⊢ φ \to Y \subseteq 𝒫 X$
	psmeasurelem.dj	$⊢ φ \to \underset{y \in Y}{Disj} y$
Assertion	psmeasurelem	$⊢ φ \to M (⋃ Y) = sum^({M ↾}_{Y})$

Proof

Step	Hyp	Ref	Expression
1		psmeasurelem.x	$⊢ φ \to X \in V$
2		psmeasurelem.h	$⊢ φ \to H : X ⟶ [0, +∞]$
3		psmeasurelem.m	$⊢ M = (x \in 𝒫 X ⟼ sum^({H ↾}_{x}))$
4		psmeasurelem.mf	$⊢ φ \to M : 𝒫 X ⟶ [0, +∞]$
5		psmeasurelem.y	$⊢ φ \to Y \subseteq 𝒫 X$
6		psmeasurelem.dj	$⊢ φ \to \underset{y \in Y}{Disj} y$
7	1	pwexd	$⊢ φ \to 𝒫 X \in V$
8		ssexg	$⊢ (Y \subseteq 𝒫 X \land 𝒫 X \in V) \to Y \in V$
9	5 7 8	syl2anc	$⊢ φ \to Y \in V$
10		simpr	$⊢ (φ \land y \in Y) \to y \in Y$
11		uniiun	$⊢ ⋃ Y = ⋃_{y \in Y} y$
12		elpwg	$⊢ Y \in V \to (Y \in 𝒫 𝒫 X \leftrightarrow Y \subseteq 𝒫 X)$
13	9 12	syl	$⊢ φ \to (Y \in 𝒫 𝒫 X \leftrightarrow Y \subseteq 𝒫 X)$
14	5 13	mpbird	$⊢ φ \to Y \in 𝒫 𝒫 X$
15		pwpwuni	$⊢ Y \in V \to (Y \in 𝒫 𝒫 X \leftrightarrow ⋃ Y \in 𝒫 X)$
16	9 15	syl	$⊢ φ \to (Y \in 𝒫 𝒫 X \leftrightarrow ⋃ Y \in 𝒫 X)$
17	14 16	mpbid	$⊢ φ \to ⋃ Y \in 𝒫 X$
18	17	elpwid	$⊢ φ \to ⋃ Y \subseteq X$
19	2 18	fssresd	$⊢ φ \to ({H ↾}_{⋃ Y}) : ⋃ Y ⟶ [0, +∞]$
20	9 10 11 19 6	sge0iun	$⊢ φ \to sum^({H ↾}_{⋃ Y}) = sum^((y \in Y ⟼ sum^({({H ↾}_{⋃ Y}) ↾}_{y})))$
21		reseq2	$⊢ x = ⋃ Y \to {H ↾}_{x} = {H ↾}_{⋃ Y}$
22	21	fveq2d	$⊢ x = ⋃ Y \to sum^({H ↾}_{x}) = sum^({H ↾}_{⋃ Y})$
23		fvexd	$⊢ φ \to sum^({H ↾}_{⋃ Y}) \in V$
24	3 22 17 23	fvmptd3	$⊢ φ \to M (⋃ Y) = sum^({H ↾}_{⋃ Y})$
25	4 5	fssresd	$⊢ φ \to ({M ↾}_{Y}) : Y ⟶ [0, +∞]$
26	25	feqmptd	$⊢ φ \to {M ↾}_{Y} = (y \in Y ⟼ ({M ↾}_{Y}) (y))$
27		fvres	$⊢ y \in Y \to ({M ↾}_{Y}) (y) = M (y)$
28	10 27	syl	$⊢ (φ \land y \in Y) \to ({M ↾}_{Y}) (y) = M (y)$
29		reseq2	$⊢ x = y \to {H ↾}_{x} = {H ↾}_{y}$
30	29	fveq2d	$⊢ x = y \to sum^({H ↾}_{x}) = sum^({H ↾}_{y})$
31	5	sselda	$⊢ (φ \land y \in Y) \to y \in 𝒫 X$
32		fvexd	$⊢ (φ \land y \in Y) \to sum^({H ↾}_{y}) \in V$
33	3 30 31 32	fvmptd3	$⊢ (φ \land y \in Y) \to M (y) = sum^({H ↾}_{y})$
34		elssuni	$⊢ y \in Y \to y \subseteq ⋃ Y$
35		resabs1	$⊢ y \subseteq ⋃ Y \to {({H ↾}_{⋃ Y}) ↾}_{y} = {H ↾}_{y}$
36	34 35	syl	$⊢ y \in Y \to {({H ↾}_{⋃ Y}) ↾}_{y} = {H ↾}_{y}$
37	36	eqcomd	$⊢ y \in Y \to {H ↾}_{y} = {({H ↾}_{⋃ Y}) ↾}_{y}$
38	37	adantl	$⊢ (φ \land y \in Y) \to {H ↾}_{y} = {({H ↾}_{⋃ Y}) ↾}_{y}$
39	38	fveq2d	$⊢ (φ \land y \in Y) \to sum^({H ↾}_{y}) = sum^({({H ↾}_{⋃ Y}) ↾}_{y})$
40	28 33 39	3eqtrd	$⊢ (φ \land y \in Y) \to ({M ↾}_{Y}) (y) = sum^({({H ↾}_{⋃ Y}) ↾}_{y})$
41	40	mpteq2dva	$⊢ φ \to (y \in Y ⟼ ({M ↾}_{Y}) (y)) = (y \in Y ⟼ sum^({({H ↾}_{⋃ Y}) ↾}_{y}))$
42	26 41	eqtrd	$⊢ φ \to {M ↾}_{Y} = (y \in Y ⟼ sum^({({H ↾}_{⋃ Y}) ↾}_{y}))$
43	42	fveq2d	$⊢ φ \to sum^({M ↾}_{Y}) = sum^((y \in Y ⟼ sum^({({H ↾}_{⋃ Y}) ↾}_{y})))$
44	20 24 43	3eqtr4d	$⊢ φ \to M (⋃ Y) = sum^({M ↾}_{Y})$

Metamath Proof Explorer

Theorem psmeasurelem

Proof