Metamath Proof Explorer


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 ( 𝜑 → ( 𝑀 𝑌 ) = ( Σ^ ‘ ( 𝑀𝑌 ) ) )