Step |
Hyp |
Ref |
Expression |
1 |
|
ofcfval3 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 𝐴 ) = ( 𝑥 ∈ dom 𝑀 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ) |
2 |
|
measfrge0 |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ) |
3 |
2
|
fdmd |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → dom 𝑀 = 𝑆 ) |
4 |
3
|
adantr |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → dom 𝑀 = 𝑆 ) |
5 |
4
|
mpteq1d |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑥 ∈ dom 𝑀 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ) |
6 |
1 5
|
eqtrd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 𝐴 ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ) |
7 |
|
measvxrge0 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) |
8 |
7
|
adantlr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) |
9 |
|
simplr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ+ ) |
10 |
8 9
|
xrpxdivcld |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ∈ ( 0 [,] +∞ ) ) |
11 |
10
|
fmpttd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ) |
12 |
|
measbase |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
13 |
|
0elsiga |
⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 ) |
14 |
12 13
|
syl |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∅ ∈ 𝑆 ) |
15 |
14
|
adantr |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ∅ ∈ 𝑆 ) |
16 |
|
ovex |
⊢ ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) ∈ V |
17 |
|
fveq2 |
⊢ ( 𝑥 = ∅ → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ ∅ ) ) |
18 |
17
|
oveq1d |
⊢ ( 𝑥 = ∅ → ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) = ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) ) |
19 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) |
20 |
18 19
|
fvmptg |
⊢ ( ( ∅ ∈ 𝑆 ∧ ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) ∈ V ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) ) |
21 |
15 16 20
|
sylancl |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) ) |
22 |
|
measvnul |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 ) |
23 |
22
|
oveq1d |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) = ( 0 /𝑒 𝐴 ) ) |
24 |
|
xdiv0rp |
⊢ ( 𝐴 ∈ ℝ+ → ( 0 /𝑒 𝐴 ) = 0 ) |
25 |
23 24
|
sylan9eq |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) = 0 ) |
26 |
21 25
|
eqtrd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ) |
27 |
|
simpll |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ) |
28 |
|
simplr |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑦 ∈ 𝒫 𝑆 ) |
29 |
|
simprl |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑦 ≼ ω ) |
30 |
|
simprr |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → Disj 𝑧 ∈ 𝑦 𝑧 ) |
31 |
|
vex |
⊢ 𝑦 ∈ V |
32 |
31
|
a1i |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) → 𝑦 ∈ V ) |
33 |
|
simplll |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑀 ∈ ( measures ‘ 𝑆 ) ) |
34 |
|
velpw |
⊢ ( 𝑦 ∈ 𝒫 𝑆 ↔ 𝑦 ⊆ 𝑆 ) |
35 |
|
ssel2 |
⊢ ( ( 𝑦 ⊆ 𝑆 ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑆 ) |
36 |
34 35
|
sylanb |
⊢ ( ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑆 ) |
37 |
36
|
adantll |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑆 ) |
38 |
|
measvxrge0 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) ) |
39 |
33 37 38
|
syl2anc |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑧 ∈ 𝑦 ) → ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) ) |
40 |
|
simplr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) → 𝐴 ∈ ℝ+ ) |
41 |
32 39 40
|
esumdivc |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) → ( Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
42 |
41
|
3ad2antr1 |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
43 |
12
|
ad2antrr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
44 |
|
simpr1 |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑦 ∈ 𝒫 𝑆 ) |
45 |
|
simpr2 |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑦 ≼ ω ) |
46 |
|
sigaclcu |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ 𝑆 ) |
47 |
43 44 45 46
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ∪ 𝑦 ∈ 𝑆 ) |
48 |
|
fveq2 |
⊢ ( 𝑥 = ∪ 𝑦 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑦 ) ) |
49 |
48
|
oveq1d |
⊢ ( 𝑥 = ∪ 𝑦 → ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) = ( ( 𝑀 ‘ ∪ 𝑦 ) /𝑒 𝐴 ) ) |
50 |
|
ovex |
⊢ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ∈ V |
51 |
49 19 50
|
fvmpt3i |
⊢ ( ∪ 𝑦 ∈ 𝑆 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = ( ( 𝑀 ‘ ∪ 𝑦 ) /𝑒 𝐴 ) ) |
52 |
47 51
|
syl |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = ( ( 𝑀 ‘ ∪ 𝑦 ) /𝑒 𝐴 ) ) |
53 |
|
simpll |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑀 ∈ ( measures ‘ 𝑆 ) ) |
54 |
|
simpr3 |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → Disj 𝑧 ∈ 𝑦 𝑧 ) |
55 |
|
measvun |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑦 ∈ 𝒫 𝑆 ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) ) |
56 |
53 44 45 54 55
|
syl112anc |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) ) |
57 |
56
|
oveq1d |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑀 ‘ ∪ 𝑦 ) /𝑒 𝐴 ) = ( Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
58 |
52 57
|
eqtrd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = ( Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
59 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑧 ) ) |
60 |
59
|
oveq1d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) = ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
61 |
60 19 50
|
fvmpt3i |
⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
62 |
36 61
|
syl |
⊢ ( ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑧 ∈ 𝑦 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
63 |
62
|
esumeq2dv |
⊢ ( 𝑦 ∈ 𝒫 𝑆 → Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
64 |
44 63
|
syl |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) ) |
65 |
42 58 64
|
3eqtr4d |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) |
66 |
27 28 29 30 65
|
syl13anc |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) |
67 |
66
|
ex |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) → ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) |
68 |
67
|
ralrimiva |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) |
69 |
|
ismeas |
⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) ) ) |
70 |
12 69
|
syl |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) ) ) |
71 |
70
|
biimprd |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ) ) |
72 |
71
|
adantr |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ) ) |
73 |
11 26 68 72
|
mp3and |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ) |
74 |
6 73
|
eqeltrd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 𝐴 ) ∈ ( measures ‘ 𝑆 ) ) |