| Step |
Hyp |
Ref |
Expression |
| 1 |
|
measinb |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) ) |
| 2 |
|
measdivcstALTV |
⊢ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /e ( 𝑀 ‘ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) ) |
| 3 |
1 2
|
stoic3 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /e ( 𝑀 ‘ 𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) ) |
| 4 |
|
eqidd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ) |
| 5 |
|
simpr |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 ) |
| 6 |
5
|
ineq1d |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = 𝑥 ) → ( 𝑦 ∩ 𝐴 ) = ( 𝑥 ∩ 𝐴 ) ) |
| 7 |
6
|
fveq2d |
⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = 𝑥 ) → ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) |
| 8 |
|
simpr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 ) |
| 9 |
|
simp1 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → 𝑀 ∈ ( measures ‘ 𝑆 ) ) |
| 10 |
9
|
adantr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝑀 ∈ ( measures ‘ 𝑆 ) ) |
| 11 |
|
measbase |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
| 12 |
10 11
|
syl |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
| 13 |
|
simp2 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → 𝐴 ∈ 𝑆 ) |
| 14 |
13
|
adantr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 ) |
| 15 |
|
inelsiga |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 ) |
| 16 |
12 8 14 15
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 ) |
| 17 |
|
measvxrge0 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑥 ∩ 𝐴 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) ) |
| 18 |
10 16 17
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) ) |
| 19 |
4 7 8 18
|
fvmptd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) = ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) |
| 20 |
19
|
oveq1d |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /e ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) /e ( 𝑀 ‘ 𝐴 ) ) ) |
| 21 |
|
iccssxr |
⊢ ( 0 [,] +∞ ) ⊆ ℝ* |
| 22 |
21 18
|
sselid |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ* ) |
| 23 |
|
simp3 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) |
| 24 |
23
|
adantr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) |
| 25 |
24
|
rpred |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) |
| 26 |
|
0xr |
⊢ 0 ∈ ℝ* |
| 27 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
| 28 |
|
iccgelb |
⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) |
| 29 |
26 27 28
|
mp3an12 |
⊢ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) |
| 30 |
18 29
|
syl |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 0 ≤ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ) |
| 31 |
|
inss2 |
⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 |
| 32 |
31
|
a1i |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 ) |
| 33 |
10 16 14 32
|
measssd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ≤ ( 𝑀 ‘ 𝐴 ) ) |
| 34 |
|
xrrege0 |
⊢ ( ( ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ ( 0 ≤ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∧ ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ≤ ( 𝑀 ‘ 𝐴 ) ) ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ) |
| 35 |
22 25 30 33 34
|
syl22anc |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ) |
| 36 |
24
|
rpne0d |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ≠ 0 ) |
| 37 |
|
rexdiv |
⊢ ( ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑀 ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) /e ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) |
| 38 |
35 25 36 37
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) /e ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) |
| 39 |
20 38
|
eqtrd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /e ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) |
| 40 |
39
|
mpteq2dva |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ ( 𝑦 ∩ 𝐴 ) ) ) ‘ 𝑥 ) /e ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) |
| 41 |
35 24
|
rerpdivcld |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ∈ ℝ ) |
| 42 |
41
|
ralrimiva |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ∈ ℝ ) |
| 43 |
|
dmmptg |
⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ∈ ℝ → dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) = 𝑆 ) |
| 44 |
42 43
|
syl |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) = 𝑆 ) |
| 45 |
44
|
fveq2d |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) = ( measures ‘ 𝑆 ) ) |
| 46 |
45
|
eqcomd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( measures ‘ 𝑆 ) = ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) ) |
| 47 |
3 40 46
|
3eltr3d |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) ) |
| 48 |
|
measbasedom |
⊢ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ∪ ran measures ↔ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) ) |
| 49 |
47 48
|
sylibr |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ∪ ran measures ) |
| 50 |
44
|
unieqd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) = ∪ 𝑆 ) |
| 51 |
50
|
fveq2d |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) = ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ 𝑆 ) ) |
| 52 |
|
eqidd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) |
| 53 |
23
|
adantr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) |
| 54 |
53
|
rpcnd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℂ ) |
| 55 |
23
|
rpne0d |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑀 ‘ 𝐴 ) ≠ 0 ) |
| 56 |
55
|
adantr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ≠ 0 ) |
| 57 |
|
simpr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → 𝑥 = ∪ 𝑆 ) |
| 58 |
57
|
ineq1d |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) = ( ∪ 𝑆 ∩ 𝐴 ) ) |
| 59 |
|
incom |
⊢ ( ∪ 𝑆 ∩ 𝐴 ) = ( 𝐴 ∩ ∪ 𝑆 ) |
| 60 |
|
elssuni |
⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ⊆ ∪ 𝑆 ) |
| 61 |
|
dfss2 |
⊢ ( 𝐴 ⊆ ∪ 𝑆 ↔ ( 𝐴 ∩ ∪ 𝑆 ) = 𝐴 ) |
| 62 |
60 61
|
sylib |
⊢ ( 𝐴 ∈ 𝑆 → ( 𝐴 ∩ ∪ 𝑆 ) = 𝐴 ) |
| 63 |
59 62
|
eqtrid |
⊢ ( 𝐴 ∈ 𝑆 → ( ∪ 𝑆 ∩ 𝐴 ) = 𝐴 ) |
| 64 |
13 63
|
syl |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( ∪ 𝑆 ∩ 𝐴 ) = 𝐴 ) |
| 65 |
64
|
adantr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( ∪ 𝑆 ∩ 𝐴 ) = 𝐴 ) |
| 66 |
58 65
|
eqtrd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑥 ∩ 𝐴 ) = 𝐴 ) |
| 67 |
66
|
fveq2d |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) = ( 𝑀 ‘ 𝐴 ) ) |
| 68 |
54 56 67
|
diveq1bd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) ∧ 𝑥 = ∪ 𝑆 ) → ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) = 1 ) |
| 69 |
|
sgon |
⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) ) |
| 70 |
|
baselsiga |
⊢ ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) → ∪ 𝑆 ∈ 𝑆 ) |
| 71 |
9 11 69 70
|
4syl |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ∪ 𝑆 ∈ 𝑆 ) |
| 72 |
|
1red |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → 1 ∈ ℝ ) |
| 73 |
52 68 71 72
|
fvmptd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ 𝑆 ) = 1 ) |
| 74 |
51 73
|
eqtrd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) = 1 ) |
| 75 |
|
elprob |
⊢ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ Prob ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ ∪ ran measures ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ) = 1 ) ) |
| 76 |
49 74 75
|
sylanbrc |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ ( 𝑥 ∩ 𝐴 ) ) / ( 𝑀 ‘ 𝐴 ) ) ) ∈ Prob ) |