Step | Hyp | Ref
| Expression |
1 | | ofcfval3 33630 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π βf/c
/π π΄) =
(π₯ β dom π β¦ ((πβπ₯) /π π΄))) |
2 | | measfrge0 33731 |
. . . . . 6
β’ (π β (measuresβπ) β π:πβΆ(0[,]+β)) |
3 | 2 | fdmd 6722 |
. . . . 5
β’ (π β (measuresβπ) β dom π = π) |
4 | 3 | adantr 480 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β β+) β dom
π = π) |
5 | 4 | mpteq1d 5236 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π₯ β dom π β¦ ((πβπ₯) /π π΄)) = (π₯ β π β¦ ((πβπ₯) /π π΄))) |
6 | 1, 5 | eqtrd 2766 |
. 2
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π βf/c
/π π΄) =
(π₯ β π β¦ ((πβπ₯) /π π΄))) |
7 | | measvxrge0 33733 |
. . . . . 6
β’ ((π β (measuresβπ) β§ π₯ β π) β (πβπ₯) β (0[,]+β)) |
8 | 7 | adantlr 712 |
. . . . 5
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π₯ β π) β (πβπ₯) β (0[,]+β)) |
9 | | simplr 766 |
. . . . 5
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π₯ β π) β π΄ β
β+) |
10 | 8, 9 | xrpxdivcld 32606 |
. . . 4
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π₯ β π) β ((πβπ₯) /π π΄) β (0[,]+β)) |
11 | 10 | fmpttd 7110 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β)) |
12 | | measbase 33725 |
. . . . . . 7
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
13 | | 0elsiga 33642 |
. . . . . . 7
β’ (π β βͺ ran sigAlgebra β β
β π) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ (π β (measuresβπ) β β
β π) |
15 | 14 | adantr 480 |
. . . . 5
β’ ((π β (measuresβπ) β§ π΄ β β+) β β
β π) |
16 | | ovex 7438 |
. . . . 5
β’ ((πββ
)
/π π΄)
β V |
17 | | fveq2 6885 |
. . . . . . 7
β’ (π₯ = β
β (πβπ₯) = (πββ
)) |
18 | 17 | oveq1d 7420 |
. . . . . 6
β’ (π₯ = β
β ((πβπ₯) /π π΄) = ((πββ
) /π π΄)) |
19 | | eqid 2726 |
. . . . . 6
β’ (π₯ β π β¦ ((πβπ₯) /π π΄)) = (π₯ β π β¦ ((πβπ₯) /π π΄)) |
20 | 18, 19 | fvmptg 6990 |
. . . . 5
β’ ((β
β π β§ ((πββ
)
/π π΄)
β V) β ((π₯ β
π β¦ ((πβπ₯) /π π΄))ββ
) = ((πββ
) /π π΄)) |
21 | 15, 16, 20 | sylancl 585 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β β+) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = ((πββ
) /π π΄)) |
22 | | measvnul 33734 |
. . . . . 6
β’ (π β (measuresβπ) β (πββ
) = 0) |
23 | 22 | oveq1d 7420 |
. . . . 5
β’ (π β (measuresβπ) β ((πββ
) /π π΄) = (0 /π
π΄)) |
24 | | xdiv0rp 32601 |
. . . . 5
β’ (π΄ β β+
β (0 /π π΄) = 0) |
25 | 23, 24 | sylan9eq 2786 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β β+) β ((πββ
)
/π π΄) =
0) |
26 | 21, 25 | eqtrd 2766 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0) |
27 | | simpll 764 |
. . . . . 6
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (π β (measuresβπ) β§ π΄ β
β+)) |
28 | | simplr 766 |
. . . . . 6
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π¦ β π« π) |
29 | | simprl 768 |
. . . . . 6
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π¦ βΌ Ο) |
30 | | simprr 770 |
. . . . . 6
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β Disj π§ β π¦ π§) |
31 | | vex 3472 |
. . . . . . . . . 10
β’ π¦ β V |
32 | 31 | a1i 11 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β π¦ β V) |
33 | | simplll 772 |
. . . . . . . . . 10
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ π§ β π¦) β π β (measuresβπ)) |
34 | | velpw 4602 |
. . . . . . . . . . . 12
β’ (π¦ β π« π β π¦ β π) |
35 | | ssel2 3972 |
. . . . . . . . . . . 12
β’ ((π¦ β π β§ π§ β π¦) β π§ β π) |
36 | 34, 35 | sylanb 580 |
. . . . . . . . . . 11
β’ ((π¦ β π« π β§ π§ β π¦) β π§ β π) |
37 | 36 | adantll 711 |
. . . . . . . . . 10
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ π§ β π¦) β π§ β π) |
38 | | measvxrge0 33733 |
. . . . . . . . . 10
β’ ((π β (measuresβπ) β§ π§ β π) β (πβπ§) β (0[,]+β)) |
39 | 33, 37, 38 | syl2anc 583 |
. . . . . . . . 9
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ π§ β π¦) β (πβπ§) β (0[,]+β)) |
40 | | simplr 766 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β π΄ β
β+) |
41 | 32, 39, 40 | esumdivc 33611 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β
(Ξ£*π§
β π¦(πβπ§) /π π΄) = Ξ£*π§ β π¦((πβπ§) /π π΄)) |
42 | 41 | 3ad2antr1 1185 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (Ξ£*π§ β π¦(πβπ§) /π π΄) = Ξ£*π§ β π¦((πβπ§) /π π΄)) |
43 | 12 | ad2antrr 723 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π β βͺ ran
sigAlgebra) |
44 | | simpr1 1191 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π¦ β π« π) |
45 | | simpr2 1192 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π¦ βΌ Ο) |
46 | | sigaclcu 33645 |
. . . . . . . . . 10
β’ ((π β βͺ ran sigAlgebra β§ π¦ β π« π β§ π¦ βΌ Ο) β βͺ π¦
β π) |
47 | 43, 44, 45, 46 | syl3anc 1368 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β βͺ π¦ β π) |
48 | | fveq2 6885 |
. . . . . . . . . . 11
β’ (π₯ = βͺ
π¦ β (πβπ₯) = (πββͺ π¦)) |
49 | 48 | oveq1d 7420 |
. . . . . . . . . 10
β’ (π₯ = βͺ
π¦ β ((πβπ₯) /π π΄) = ((πββͺ π¦) /π π΄)) |
50 | | ovex 7438 |
. . . . . . . . . 10
β’ ((πβπ₯) /π π΄) β V |
51 | 49, 19, 50 | fvmpt3i 6997 |
. . . . . . . . 9
β’ (βͺ π¦
β π β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = ((πββͺ π¦) /π π΄)) |
52 | 47, 51 | syl 17 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = ((πββͺ π¦) /π π΄)) |
53 | | simpll 764 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π β (measuresβπ)) |
54 | | simpr3 1193 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β Disj π§ β π¦ π§) |
55 | | measvun 33737 |
. . . . . . . . . 10
β’ ((π β (measuresβπ) β§ π¦ β π« π β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (πββͺ π¦) = Ξ£*π§ β π¦(πβπ§)) |
56 | 53, 44, 45, 54, 55 | syl112anc 1371 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (πββͺ π¦) = Ξ£*π§ β π¦(πβπ§)) |
57 | 56 | oveq1d 7420 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((πββͺ π¦) /π π΄) = (Ξ£*π§ β π¦(πβπ§) /π π΄)) |
58 | 52, 57 | eqtrd 2766 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = (Ξ£*π§ β π¦(πβπ§) /π π΄)) |
59 | | fveq2 6885 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (πβπ₯) = (πβπ§)) |
60 | 59 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (π₯ = π§ β ((πβπ₯) /π π΄) = ((πβπ§) /π π΄)) |
61 | 60, 19, 50 | fvmpt3i 6997 |
. . . . . . . . . 10
β’ (π§ β π β ((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§) = ((πβπ§) /π π΄)) |
62 | 36, 61 | syl 17 |
. . . . . . . . 9
β’ ((π¦ β π« π β§ π§ β π¦) β ((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§) = ((πβπ§) /π π΄)) |
63 | 62 | esumeq2dv 33566 |
. . . . . . . 8
β’ (π¦ β π« π β Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§) = Ξ£*π§ β π¦((πβπ§) /π π΄)) |
64 | 44, 63 | syl 17 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§) = Ξ£*π§ β π¦((πβπ§) /π π΄)) |
65 | 42, 58, 64 | 3eqtr4d 2776 |
. . . . . 6
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§)) |
66 | 27, 28, 29, 30, 65 | syl13anc 1369 |
. . . . 5
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§)) |
67 | 66 | ex 412 |
. . . 4
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β ((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))) |
68 | 67 | ralrimiva 3140 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β
βπ¦ β π«
π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))) |
69 | | ismeas 33727 |
. . . . . 6
β’ (π β βͺ ran sigAlgebra β ((π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ) β ((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))))) |
70 | 12, 69 | syl 17 |
. . . . 5
β’ (π β (measuresβπ) β ((π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ) β ((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))))) |
71 | 70 | biimprd 247 |
. . . 4
β’ (π β (measuresβπ) β (((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))) β (π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ))) |
72 | 71 | adantr 480 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β (((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))) β (π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ))) |
73 | 11, 26, 68, 72 | mp3and 1460 |
. 2
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ)) |
74 | 6, 73 | eqeltrd 2827 |
1
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π βf/c
/π π΄)
β (measuresβπ)) |