Step | Hyp | Ref
| Expression |
1 | | simp2 1128 |
. 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → 𝑇 ∈ ∪ ran
sigAlgebra) |
2 | | measfrge0 30864 |
. . . . 5
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞)) |
3 | 2 | 3ad2ant1 1124 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → 𝑀:𝑆⟶(0[,]+∞)) |
4 | | simp3 1129 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → 𝑇 ⊆ 𝑆) |
5 | 3, 4 | fssresd 6321 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → (𝑀 ↾ 𝑇):𝑇⟶(0[,]+∞)) |
6 | | 0elsiga 30775 |
. . . . 5
⊢ (𝑇 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑇) |
7 | | fvres 6465 |
. . . . 5
⊢ (∅
∈ 𝑇 → ((𝑀 ↾ 𝑇)‘∅) = (𝑀‘∅)) |
8 | 1, 6, 7 | 3syl 18 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → ((𝑀 ↾ 𝑇)‘∅) = (𝑀‘∅)) |
9 | | measvnul 30867 |
. . . . 5
⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0) |
10 | 9 | 3ad2ant1 1124 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → (𝑀‘∅) =
0) |
11 | 8, 10 | eqtrd 2814 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → ((𝑀 ↾ 𝑇)‘∅) = 0) |
12 | | simp11 1217 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑀 ∈ (measures‘𝑆)) |
13 | | simp13 1219 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑇 ⊆ 𝑆) |
14 | | simp2 1128 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑇) |
15 | | sspwb 5149 |
. . . . . . . . 9
⊢ (𝑇 ⊆ 𝑆 ↔ 𝒫 𝑇 ⊆ 𝒫 𝑆) |
16 | | ssel2 3816 |
. . . . . . . . 9
⊢
((𝒫 𝑇
⊆ 𝒫 𝑆 ∧
𝑥 ∈ 𝒫 𝑇) → 𝑥 ∈ 𝒫 𝑆) |
17 | 15, 16 | sylanb 576 |
. . . . . . . 8
⊢ ((𝑇 ⊆ 𝑆 ∧ 𝑥 ∈ 𝒫 𝑇) → 𝑥 ∈ 𝒫 𝑆) |
18 | 13, 14, 17 | syl2anc 579 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑆) |
19 | | simp3 1129 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) |
20 | | measvun 30870 |
. . . . . . 7
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑥 ∈ 𝒫 𝑆 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
21 | 12, 18, 19, 20 | syl3anc 1439 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
22 | 1 | 3ad2ant1 1124 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑇 ∈ ∪ ran
sigAlgebra) |
23 | | simp3l 1215 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑥 ≼ ω) |
24 | | sigaclcu 30778 |
. . . . . . . 8
⊢ ((𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝑇) |
25 | 22, 14, 23, 24 | syl3anc 1439 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ∪ 𝑥 ∈ 𝑇) |
26 | | fvres 6465 |
. . . . . . 7
⊢ (∪ 𝑥
∈ 𝑇 → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = (𝑀‘∪ 𝑥)) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = (𝑀‘∪ 𝑥)) |
28 | | elpwi 4389 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑇 → 𝑥 ⊆ 𝑇) |
29 | 28 | sselda 3821 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 𝑇 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑇) |
30 | 29 | adantll 704 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑇) |
31 | | fvres 6465 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑇 → ((𝑀 ↾ 𝑇)‘𝑦) = (𝑀‘𝑦)) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) ∧ 𝑦 ∈ 𝑥) → ((𝑀 ↾ 𝑇)‘𝑦) = (𝑀‘𝑦)) |
33 | 32 | esumeq2dv 30698 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) → Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
34 | 33 | 3adant3 1123 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
35 | 21, 27, 34 | 3eqtr4d 2824 |
. . . . 5
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦)) |
36 | 35 | 3expia 1111 |
. . . 4
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦))) |
37 | 36 | ralrimiva 3148 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦))) |
38 | 5, 11, 37 | 3jca 1119 |
. 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → ((𝑀 ↾ 𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀 ↾ 𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦)))) |
39 | | ismeas 30860 |
. . 3
⊢ (𝑇 ∈ ∪ ran sigAlgebra → ((𝑀 ↾ 𝑇) ∈ (measures‘𝑇) ↔ ((𝑀 ↾ 𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀 ↾ 𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦))))) |
40 | 39 | biimprd 240 |
. 2
⊢ (𝑇 ∈ ∪ ran sigAlgebra → (((𝑀 ↾ 𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀 ↾ 𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦))) → (𝑀 ↾ 𝑇) ∈ (measures‘𝑇))) |
41 | 1, 38, 40 | sylc 65 |
1
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → (𝑀 ↾ 𝑇) ∈ (measures‘𝑇)) |