Theorem 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	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	psmeasurelem.h	⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ( 0 [,] +∞ ) )
	psmeasurelem.m	⊢ 𝑀 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ( Σ^ ‘ ( 𝐻 ↾ 𝑥 ) ) )
	psmeasurelem.mf	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
	psmeasurelem.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝒫 𝑋 )
	psmeasurelem.dj	⊢ ( 𝜑 → Disj 𝑦 ∈ 𝑌 𝑦 )
Assertion	psmeasurelem	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑌 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psmeasurelem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		psmeasurelem.h	⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3		psmeasurelem.m	⊢ 𝑀 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ( Σ^ ‘ ( 𝐻 ↾ 𝑥 ) ) )
4		psmeasurelem.mf	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
5		psmeasurelem.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝒫 𝑋 )
6		psmeasurelem.dj	⊢ ( 𝜑 → Disj 𝑦 ∈ 𝑌 𝑦 )
7	1	pwexd	⊢ ( 𝜑 → 𝒫 𝑋 ∈ V )
8		ssexg	⊢ ( ( 𝑌 ⊆ 𝒫 𝑋 ∧ 𝒫 𝑋 ∈ V ) → 𝑌 ∈ V )
9	5 7 8	syl2anc	⊢ ( 𝜑 → 𝑌 ∈ V )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
11		uniiun	⊢ ∪ 𝑌 = ∪ 𝑦 ∈ 𝑌 𝑦
12		elpwg	⊢ ( 𝑌 ∈ V → ( 𝑌 ∈ 𝒫 𝒫 𝑋 ↔ 𝑌 ⊆ 𝒫 𝑋 ) )
13	9 12	syl	⊢ ( 𝜑 → ( 𝑌 ∈ 𝒫 𝒫 𝑋 ↔ 𝑌 ⊆ 𝒫 𝑋 ) )
14	5 13	mpbird	⊢ ( 𝜑 → 𝑌 ∈ 𝒫 𝒫 𝑋 )
15		pwpwuni	⊢ ( 𝑌 ∈ V → ( 𝑌 ∈ 𝒫 𝒫 𝑋 ↔ ∪ 𝑌 ∈ 𝒫 𝑋 ) )
16	9 15	syl	⊢ ( 𝜑 → ( 𝑌 ∈ 𝒫 𝒫 𝑋 ↔ ∪ 𝑌 ∈ 𝒫 𝑋 ) )
17	14 16	mpbid	⊢ ( 𝜑 → ∪ 𝑌 ∈ 𝒫 𝑋 )
18	17	elpwid	⊢ ( 𝜑 → ∪ 𝑌 ⊆ 𝑋 )
19	2 18	fssresd	⊢ ( 𝜑 → ( 𝐻 ↾ ∪ 𝑌 ) : ∪ 𝑌 ⟶ ( 0 [,] +∞ ) )
20	9 10 11 19 6	sge0iun	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐻 ↾ ∪ 𝑌 ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝑌 ↦ ( Σ^ ‘ ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) ) ) ) )
21		reseq2	⊢ ( 𝑥 = ∪ 𝑌 → ( 𝐻 ↾ 𝑥 ) = ( 𝐻 ↾ ∪ 𝑌 ) )
22	21	fveq2d	⊢ ( 𝑥 = ∪ 𝑌 → ( Σ^ ‘ ( 𝐻 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝐻 ↾ ∪ 𝑌 ) ) )
23		fvexd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐻 ↾ ∪ 𝑌 ) ) ∈ V )
24	3 22 17 23	fvmptd3	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑌 ) = ( Σ^ ‘ ( 𝐻 ↾ ∪ 𝑌 ) ) )
25	4 5	fssresd	⊢ ( 𝜑 → ( 𝑀 ↾ 𝑌 ) : 𝑌 ⟶ ( 0 [,] +∞ ) )
26	25	feqmptd	⊢ ( 𝜑 → ( 𝑀 ↾ 𝑌 ) = ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑀 ↾ 𝑌 ) ‘ 𝑦 ) ) )
27		fvres	⊢ ( 𝑦 ∈ 𝑌 → ( ( 𝑀 ↾ 𝑌 ) ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) )
28	10 27	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑀 ↾ 𝑌 ) ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) )
29		reseq2	⊢ ( 𝑥 = 𝑦 → ( 𝐻 ↾ 𝑥 ) = ( 𝐻 ↾ 𝑦 ) )
30	29	fveq2d	⊢ ( 𝑥 = 𝑦 → ( Σ^ ‘ ( 𝐻 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝐻 ↾ 𝑦 ) ) )
31	5	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝒫 𝑋 )
32		fvexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( Σ^ ‘ ( 𝐻 ↾ 𝑦 ) ) ∈ V )
33	3 30 31 32	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑀 ‘ 𝑦 ) = ( Σ^ ‘ ( 𝐻 ↾ 𝑦 ) ) )
34		elssuni	⊢ ( 𝑦 ∈ 𝑌 → 𝑦 ⊆ ∪ 𝑌 )
35		resabs1	⊢ ( 𝑦 ⊆ ∪ 𝑌 → ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) = ( 𝐻 ↾ 𝑦 ) )
36	34 35	syl	⊢ ( 𝑦 ∈ 𝑌 → ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) = ( 𝐻 ↾ 𝑦 ) )
37	36	eqcomd	⊢ ( 𝑦 ∈ 𝑌 → ( 𝐻 ↾ 𝑦 ) = ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐻 ↾ 𝑦 ) = ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) )
39	38	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( Σ^ ‘ ( 𝐻 ↾ 𝑦 ) ) = ( Σ^ ‘ ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) ) )
40	28 33 39	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑀 ↾ 𝑌 ) ‘ 𝑦 ) = ( Σ^ ‘ ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) ) )
41	40	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑀 ↾ 𝑌 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( Σ^ ‘ ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) ) ) )
42	26 41	eqtrd	⊢ ( 𝜑 → ( 𝑀 ↾ 𝑌 ) = ( 𝑦 ∈ 𝑌 ↦ ( Σ^ ‘ ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) ) ) )
43	42	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑀 ↾ 𝑌 ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝑌 ↦ ( Σ^ ‘ ( ( 𝐻 ↾ ∪ 𝑌 ) ↾ 𝑦 ) ) ) ) )
44	20 24 43	3eqtr4d	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑌 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑌 ) ) )