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