Step | Hyp | Ref
| Expression |
1 | | simp2 1062 |
. 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → 𝑇 ∈ ∪ ran
sigAlgebra) |
2 | | measfrge0 30266 |
. . . . 5
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞)) |
3 | 2 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → 𝑀:𝑆⟶(0[,]+∞)) |
4 | | simp3 1063 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → 𝑇 ⊆ 𝑆) |
5 | 3, 4 | fssresd 6071 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → (𝑀 ↾ 𝑇):𝑇⟶(0[,]+∞)) |
6 | | 0elsiga 30177 |
. . . . 5
⊢ (𝑇 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑇) |
7 | | fvres 6207 |
. . . . 5
⊢ (∅
∈ 𝑇 → ((𝑀 ↾ 𝑇)‘∅) = (𝑀‘∅)) |
8 | 1, 6, 7 | 3syl 18 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → ((𝑀 ↾ 𝑇)‘∅) = (𝑀‘∅)) |
9 | | measvnul 30269 |
. . . . 5
⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0) |
10 | 9 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → (𝑀‘∅) =
0) |
11 | 8, 10 | eqtrd 2656 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → ((𝑀 ↾ 𝑇)‘∅) = 0) |
12 | | simp11 1091 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑀 ∈ (measures‘𝑆)) |
13 | | simp13 1093 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑇 ⊆ 𝑆) |
14 | | simp2 1062 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑇) |
15 | | sspwb 4917 |
. . . . . . . . 9
⊢ (𝑇 ⊆ 𝑆 ↔ 𝒫 𝑇 ⊆ 𝒫 𝑆) |
16 | | ssel2 3598 |
. . . . . . . . 9
⊢
((𝒫 𝑇
⊆ 𝒫 𝑆 ∧
𝑥 ∈ 𝒫 𝑇) → 𝑥 ∈ 𝒫 𝑆) |
17 | 15, 16 | sylanb 489 |
. . . . . . . 8
⊢ ((𝑇 ⊆ 𝑆 ∧ 𝑥 ∈ 𝒫 𝑇) → 𝑥 ∈ 𝒫 𝑆) |
18 | 13, 14, 17 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑆) |
19 | | simp3 1063 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) |
20 | | measvun 30272 |
. . . . . . 7
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑥 ∈ 𝒫 𝑆 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
21 | 12, 18, 19, 20 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
22 | 1 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑇 ∈ ∪ ran
sigAlgebra) |
23 | | simp3l 1089 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → 𝑥 ≼ ω) |
24 | | sigaclcu 30180 |
. . . . . . . 8
⊢ ((𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝑇) |
25 | 22, 14, 23, 24 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ∪ 𝑥 ∈ 𝑇) |
26 | | fvres 6207 |
. . . . . . 7
⊢ (∪ 𝑥
∈ 𝑇 → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = (𝑀‘∪ 𝑥)) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = (𝑀‘∪ 𝑥)) |
28 | | elpwi 4168 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑇 → 𝑥 ⊆ 𝑇) |
29 | 28 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 𝑇 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑇) |
30 | 29 | adantll 750 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑇) |
31 | | fvres 6207 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑇 → ((𝑀 ↾ 𝑇)‘𝑦) = (𝑀‘𝑦)) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) ∧ 𝑦 ∈ 𝑥) → ((𝑀 ↾ 𝑇)‘𝑦) = (𝑀‘𝑦)) |
33 | 32 | esumeq2dv 30100 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) → Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
34 | 33 | 3adant3 1081 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
35 | 21, 27, 34 | 3eqtr4d 2666 |
. . . . 5
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦)) |
36 | 35 | 3expia 1267 |
. . . 4
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦))) |
37 | 36 | ralrimiva 2966 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦))) |
38 | 5, 11, 37 | 3jca 1242 |
. 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → ((𝑀 ↾ 𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀 ↾ 𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦)))) |
39 | | ismeas 30262 |
. . 3
⊢ (𝑇 ∈ ∪ ran sigAlgebra → ((𝑀 ↾ 𝑇) ∈ (measures‘𝑇) ↔ ((𝑀 ↾ 𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀 ↾ 𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦))))) |
40 | 39 | biimprd 238 |
. 2
⊢ (𝑇 ∈ ∪ ran sigAlgebra → (((𝑀 ↾ 𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀 ↾ 𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑀 ↾ 𝑇)‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥((𝑀 ↾ 𝑇)‘𝑦))) → (𝑀 ↾ 𝑇) ∈ (measures‘𝑇))) |
41 | 1, 38, 40 | sylc 65 |
1
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran
sigAlgebra ∧ 𝑇 ⊆
𝑆) → (𝑀 ↾ 𝑇) ∈ (measures‘𝑇)) |