Step | Hyp | Ref
| Expression |
1 | | measinb 31751 |
. . . . 5
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴))) ∈ (measures‘𝑆)) |
2 | | measdivcstALTV 31755 |
. . . . 5
⊢ (((𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴))) ∈ (measures‘𝑆) ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ (((𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴)))‘𝑥) /𝑒 (𝑀‘𝐴))) ∈ (measures‘𝑆)) |
3 | 1, 2 | stoic3 1783 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ (((𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴)))‘𝑥) /𝑒 (𝑀‘𝐴))) ∈ (measures‘𝑆)) |
4 | | eqidd 2739 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴))) = (𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴)))) |
5 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
6 | 5 | ineq1d 4100 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 = 𝑥) → (𝑦 ∩ 𝐴) = (𝑥 ∩ 𝐴)) |
7 | 6 | fveq2d 6672 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 = 𝑥) → (𝑀‘(𝑦 ∩ 𝐴)) = (𝑀‘(𝑥 ∩ 𝐴))) |
8 | | simpr 488 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
9 | | simp1 1137 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → 𝑀 ∈ (measures‘𝑆)) |
10 | 9 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ (measures‘𝑆)) |
11 | | measbase 31727 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑆 ∈ ∪ ran
sigAlgebra) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → 𝑆 ∈ ∪ ran
sigAlgebra) |
13 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → 𝐴 ∈ 𝑆) |
14 | 13 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑆) |
15 | | inelsiga 31665 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (𝑥 ∩ 𝐴) ∈ 𝑆) |
16 | 12, 8, 14, 15 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∩ 𝐴) ∈ 𝑆) |
17 | | measvxrge0 31735 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑥 ∩ 𝐴) ∈ 𝑆) → (𝑀‘(𝑥 ∩ 𝐴)) ∈ (0[,]+∞)) |
18 | 10, 16, 17 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑀‘(𝑥 ∩ 𝐴)) ∈ (0[,]+∞)) |
19 | 4, 7, 8, 18 | fvmptd 6776 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → ((𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴)))‘𝑥) = (𝑀‘(𝑥 ∩ 𝐴))) |
20 | 19 | oveq1d 7179 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (((𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴)))‘𝑥) /𝑒 (𝑀‘𝐴)) = ((𝑀‘(𝑥 ∩ 𝐴)) /𝑒 (𝑀‘𝐴))) |
21 | | iccssxr 12897 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
22 | 21, 18 | sseldi 3873 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑀‘(𝑥 ∩ 𝐴)) ∈
ℝ*) |
23 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑀‘𝐴) ∈
ℝ+) |
24 | 23 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑀‘𝐴) ∈
ℝ+) |
25 | 24 | rpred 12507 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑀‘𝐴) ∈ ℝ) |
26 | | 0xr 10759 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
27 | | pnfxr 10766 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
28 | | iccgelb 12870 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝑀‘(𝑥 ∩ 𝐴)) ∈ (0[,]+∞)) → 0 ≤
(𝑀‘(𝑥 ∩ 𝐴))) |
29 | 26, 27, 28 | mp3an12 1452 |
. . . . . . . . 9
⊢ ((𝑀‘(𝑥 ∩ 𝐴)) ∈ (0[,]+∞) → 0 ≤
(𝑀‘(𝑥 ∩ 𝐴))) |
30 | 18, 29 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → 0 ≤ (𝑀‘(𝑥 ∩ 𝐴))) |
31 | | inss2 4118 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴 |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∩ 𝐴) ⊆ 𝐴) |
33 | 10, 16, 14, 32 | measssd 31745 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑀‘(𝑥 ∩ 𝐴)) ≤ (𝑀‘𝐴)) |
34 | | xrrege0 12643 |
. . . . . . . 8
⊢ ((((𝑀‘(𝑥 ∩ 𝐴)) ∈ ℝ* ∧ (𝑀‘𝐴) ∈ ℝ) ∧ (0 ≤ (𝑀‘(𝑥 ∩ 𝐴)) ∧ (𝑀‘(𝑥 ∩ 𝐴)) ≤ (𝑀‘𝐴))) → (𝑀‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
35 | 22, 25, 30, 33, 34 | syl22anc 838 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑀‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
36 | 24 | rpne0d 12512 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (𝑀‘𝐴) ≠ 0) |
37 | | rexdiv 30767 |
. . . . . . 7
⊢ (((𝑀‘(𝑥 ∩ 𝐴)) ∈ ℝ ∧ (𝑀‘𝐴) ∈ ℝ ∧ (𝑀‘𝐴) ≠ 0) → ((𝑀‘(𝑥 ∩ 𝐴)) /𝑒 (𝑀‘𝐴)) = ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) |
38 | 35, 25, 36, 37 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → ((𝑀‘(𝑥 ∩ 𝐴)) /𝑒 (𝑀‘𝐴)) = ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) |
39 | 20, 38 | eqtrd 2773 |
. . . . 5
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → (((𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴)))‘𝑥) /𝑒 (𝑀‘𝐴)) = ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) |
40 | 39 | mpteq2dva 5122 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ (((𝑦 ∈ 𝑆 ↦ (𝑀‘(𝑦 ∩ 𝐴)))‘𝑥) /𝑒 (𝑀‘𝐴))) = (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))) |
41 | 35, 24 | rerpdivcld 12538 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 ∈ 𝑆) → ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)) ∈ ℝ) |
42 | 41 | ralrimiva 3096 |
. . . . . . 7
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) →
∀𝑥 ∈ 𝑆 ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)) ∈ ℝ) |
43 | | dmmptg 6068 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑆 ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)) ∈ ℝ → dom (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) = 𝑆) |
44 | 42, 43 | syl 17 |
. . . . . 6
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → dom
(𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) = 𝑆) |
45 | 44 | fveq2d 6672 |
. . . . 5
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) →
(measures‘dom (𝑥
∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))) = (measures‘𝑆)) |
46 | 45 | eqcomd 2744 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) →
(measures‘𝑆) =
(measures‘dom (𝑥
∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))))) |
47 | 3, 40, 46 | 3eltr3d 2847 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ (measures‘dom (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))))) |
48 | | measbasedom 31732 |
. . 3
⊢ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ ∪ ran
measures ↔ (𝑥 ∈
𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ (measures‘dom (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))))) |
49 | 47, 48 | sylibr 237 |
. 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ ∪ ran
measures) |
50 | 44 | unieqd 4807 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → ∪ dom (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) = ∪ 𝑆) |
51 | 50 | fveq2d 6672 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))‘∪ dom
(𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))) = ((𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))‘∪ 𝑆)) |
52 | | eqidd 2739 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) = (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))) |
53 | 23 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → (𝑀‘𝐴) ∈
ℝ+) |
54 | 53 | rpcnd 12509 |
. . . . 5
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → (𝑀‘𝐴) ∈ ℂ) |
55 | 23 | rpne0d 12512 |
. . . . . 6
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑀‘𝐴) ≠ 0) |
56 | 55 | adantr 484 |
. . . . 5
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → (𝑀‘𝐴) ≠ 0) |
57 | | simpr 488 |
. . . . . . . 8
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → 𝑥 = ∪
𝑆) |
58 | 57 | ineq1d 4100 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → (𝑥 ∩ 𝐴) = (∪ 𝑆 ∩ 𝐴)) |
59 | | incom 4089 |
. . . . . . . . . 10
⊢ (∪ 𝑆
∩ 𝐴) = (𝐴 ∩ ∪ 𝑆) |
60 | | elssuni 4825 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑆 → 𝐴 ⊆ ∪ 𝑆) |
61 | | df-ss 3858 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ ∪ 𝑆
↔ (𝐴 ∩ ∪ 𝑆) =
𝐴) |
62 | 60, 61 | sylib 221 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → (𝐴 ∩ ∪ 𝑆) = 𝐴) |
63 | 59, 62 | syl5eq 2785 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑆 → (∪ 𝑆 ∩ 𝐴) = 𝐴) |
64 | 13, 63 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (∪ 𝑆
∩ 𝐴) = 𝐴) |
65 | 64 | adantr 484 |
. . . . . . 7
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → (∪ 𝑆
∩ 𝐴) = 𝐴) |
66 | 58, 65 | eqtrd 2773 |
. . . . . 6
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → (𝑥 ∩ 𝐴) = 𝐴) |
67 | 66 | fveq2d 6672 |
. . . . 5
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → (𝑀‘(𝑥 ∩ 𝐴)) = (𝑀‘𝐴)) |
68 | 54, 56, 67 | diveq1bd 11535 |
. . . 4
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) ∧ 𝑥 = ∪
𝑆) → ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)) = 1) |
69 | | sgon 31654 |
. . . . 5
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆)) |
70 | | baselsiga 31645 |
. . . . 5
⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆)
→ ∪ 𝑆 ∈ 𝑆) |
71 | 9, 11, 69, 70 | 4syl 19 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → ∪ 𝑆
∈ 𝑆) |
72 | | 1red 10713 |
. . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → 1
∈ ℝ) |
73 | 52, 68, 71, 72 | fvmptd 6776 |
. . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))‘∪ 𝑆) = 1) |
74 | 51, 73 | eqtrd 2773 |
. 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → ((𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))‘∪ dom
(𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))) = 1) |
75 | | elprob 31938 |
. 2
⊢ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ Prob ↔ ((𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ ∪ ran
measures ∧ ((𝑥 ∈
𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))‘∪ dom
(𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴)))) = 1)) |
76 | 49, 74, 75 | sylanbrc 586 |
1
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ Prob) |