Step | Hyp | Ref
| Expression |
1 | | ofcfval3 29491 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑀∘𝑓/𝑐
/𝑒 𝐴) =
(𝑥 ∈ dom 𝑀 ↦ ((𝑀‘𝑥) /𝑒 𝐴))) |
2 | | measfrge0 29593 |
. . . . . 6
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞)) |
3 | | fdm 5964 |
. . . . . 6
⊢ (𝑀:𝑆⟶(0[,]+∞) → dom 𝑀 = 𝑆) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝑀 ∈ (measures‘𝑆) → dom 𝑀 = 𝑆) |
5 | 4 | adantr 480 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → dom
𝑀 = 𝑆) |
6 | 5 | mpteq1d 4666 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥 ∈ dom 𝑀 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) = (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))) |
7 | 1, 6 | eqtrd 2644 |
. 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑀∘𝑓/𝑐
/𝑒 𝐴) =
(𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))) |
8 | | measvxrge0 29595 |
. . . . . 6
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑀‘𝑥) ∈ (0[,]+∞)) |
9 | 8 | adantlr 747 |
. . . . 5
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑀‘𝑥) ∈ (0[,]+∞)) |
10 | | simplr 788 |
. . . . 5
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈
ℝ+) |
11 | 9, 10 | xrpxdivcld 28974 |
. . . 4
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → ((𝑀‘𝑥) /𝑒 𝐴) ∈ (0[,]+∞)) |
12 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) = (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) |
13 | 11, 12 | fmptd 6292 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞)) |
14 | | measbase 29587 |
. . . . . . 7
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑆 ∈ ∪ ran
sigAlgebra) |
15 | | 0elsiga 29504 |
. . . . . . 7
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (𝑀 ∈ (measures‘𝑆) → ∅ ∈ 𝑆) |
17 | 16 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ∅
∈ 𝑆) |
18 | | ovex 6577 |
. . . . 5
⊢ ((𝑀‘∅)
/𝑒 𝐴)
∈ V |
19 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑀‘𝑥) = (𝑀‘∅)) |
20 | 19 | oveq1d 6564 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝑀‘𝑥) /𝑒 𝐴) = ((𝑀‘∅) /𝑒 𝐴)) |
21 | 20, 12 | fvmptg 6189 |
. . . . 5
⊢ ((∅
∈ 𝑆 ∧ ((𝑀‘∅)
/𝑒 𝐴)
∈ V) → ((𝑥 ∈
𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∅) = ((𝑀‘∅) /𝑒 𝐴)) |
22 | 17, 18, 21 | sylancl 693 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∅) = ((𝑀‘∅) /𝑒 𝐴)) |
23 | | measvnul 29596 |
. . . . . 6
⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0) |
24 | 23 | oveq1d 6564 |
. . . . 5
⊢ (𝑀 ∈ (measures‘𝑆) → ((𝑀‘∅) /𝑒 𝐴) = (0 /𝑒
𝐴)) |
25 | | xdiv0rp 28969 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (0 /𝑒 𝐴) = 0) |
26 | 24, 25 | sylan9eq 2664 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ((𝑀‘∅)
/𝑒 𝐴) =
0) |
27 | 22, 26 | eqtrd 2644 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∅) = 0) |
28 | | simpll 786 |
. . . . . 6
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → (𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈
ℝ+)) |
29 | | simplr 788 |
. . . . . 6
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → 𝑦 ∈ 𝒫 𝑆) |
30 | | simprl 790 |
. . . . . 6
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → 𝑦 ≼ ω) |
31 | | simprr 792 |
. . . . . 6
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → Disj 𝑧 ∈ 𝑦 𝑧) |
32 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
33 | 32 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) → 𝑦 ∈ V) |
34 | | simplll 794 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ 𝑧 ∈ 𝑦) → 𝑀 ∈ (measures‘𝑆)) |
35 | | selpw 4115 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 𝑆 ↔ 𝑦 ⊆ 𝑆) |
36 | | ssel2 3563 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ 𝑆 ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑆) |
37 | 35, 36 | sylanb 488 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝒫 𝑆 ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑆) |
38 | 37 | adantll 746 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑆) |
39 | | measvxrge0 29595 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑀‘𝑧) ∈ (0[,]+∞)) |
40 | 34, 38, 39 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ 𝑧 ∈ 𝑦) → (𝑀‘𝑧) ∈ (0[,]+∞)) |
41 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) → 𝐴 ∈
ℝ+) |
42 | 33, 40, 41 | esumdivc 29472 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) →
(Σ*𝑧
∈ 𝑦(𝑀‘𝑧) /𝑒 𝐴) = Σ*𝑧 ∈ 𝑦((𝑀‘𝑧) /𝑒 𝐴)) |
43 | 42 | 3ad2antr1 1219 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → (Σ*𝑧 ∈ 𝑦(𝑀‘𝑧) /𝑒 𝐴) = Σ*𝑧 ∈ 𝑦((𝑀‘𝑧) /𝑒 𝐴)) |
44 | 14 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → 𝑆 ∈ ∪ ran
sigAlgebra) |
45 | | simpr1 1060 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → 𝑦 ∈ 𝒫 𝑆) |
46 | | simpr2 1061 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → 𝑦 ≼ ω) |
47 | | sigaclcu 29507 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω) → ∪ 𝑦
∈ 𝑆) |
48 | 44, 45, 46, 47 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → ∪ 𝑦 ∈ 𝑆) |
49 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = ∪
𝑦 → (𝑀‘𝑥) = (𝑀‘∪ 𝑦)) |
50 | 49 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑥 = ∪
𝑦 → ((𝑀‘𝑥) /𝑒 𝐴) = ((𝑀‘∪ 𝑦) /𝑒 𝐴)) |
51 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥) /𝑒 𝐴) ∈ V |
52 | 50, 12, 51 | fvmpt3i 6196 |
. . . . . . . . 9
⊢ (∪ 𝑦
∈ 𝑆 → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = ((𝑀‘∪ 𝑦) /𝑒 𝐴)) |
53 | 48, 52 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = ((𝑀‘∪ 𝑦) /𝑒 𝐴)) |
54 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → 𝑀 ∈ (measures‘𝑆)) |
55 | | simpr3 1062 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → Disj 𝑧 ∈ 𝑦 𝑧) |
56 | | measvun 29599 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑦 ∈ 𝒫 𝑆 ∧ (𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → (𝑀‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦(𝑀‘𝑧)) |
57 | 54, 45, 46, 55, 56 | syl112anc 1322 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → (𝑀‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦(𝑀‘𝑧)) |
58 | 57 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → ((𝑀‘∪ 𝑦) /𝑒 𝐴) = (Σ*𝑧 ∈ 𝑦(𝑀‘𝑧) /𝑒 𝐴)) |
59 | 53, 58 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = (Σ*𝑧 ∈ 𝑦(𝑀‘𝑧) /𝑒 𝐴)) |
60 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑀‘𝑥) = (𝑀‘𝑧)) |
61 | 60 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((𝑀‘𝑥) /𝑒 𝐴) = ((𝑀‘𝑧) /𝑒 𝐴)) |
62 | 61, 12, 51 | fvmpt3i 6196 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧) = ((𝑀‘𝑧) /𝑒 𝐴)) |
63 | 37, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝒫 𝑆 ∧ 𝑧 ∈ 𝑦) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧) = ((𝑀‘𝑧) /𝑒 𝐴)) |
64 | 63 | esumeq2dv 29427 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝒫 𝑆 → Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧) = Σ*𝑧 ∈ 𝑦((𝑀‘𝑧) /𝑒 𝐴)) |
65 | 45, 64 | syl 17 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧) = Σ*𝑧 ∈ 𝑦((𝑀‘𝑧) /𝑒 𝐴)) |
66 | 43, 59, 65 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧)) |
67 | 28, 29, 30, 31, 66 | syl13anc 1320 |
. . . . 5
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧)) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧)) |
68 | 67 | ex 449 |
. . . 4
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) → ((𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧))) |
69 | 68 | ralrimiva 2949 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) →
∀𝑦 ∈ 𝒫
𝑆((𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧))) |
70 | | ismeas 29589 |
. . . . . 6
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆) ↔ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧))))) |
71 | 14, 70 | syl 17 |
. . . . 5
⊢ (𝑀 ∈ (measures‘𝑆) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆) ↔ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧))))) |
72 | 71 | biimprd 237 |
. . . 4
⊢ (𝑀 ∈ (measures‘𝑆) → (((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧))) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆))) |
73 | 72 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘∪ 𝑦) = Σ*𝑧 ∈ 𝑦((𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴))‘𝑧))) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆))) |
74 | 13, 27, 69, 73 | mp3and 1419 |
. 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆)) |
75 | 7, 74 | eqeltrd 2688 |
1
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑀∘𝑓/𝑐
/𝑒 𝐴)
∈ (measures‘𝑆)) |