Step | Hyp | Ref
| Expression |
1 | | funmpt 6543 |
. . . . . 6
β’ Fun
(π₯ β π β¦ ((πβπ₯) /π π΄)) |
2 | | ovex 7394 |
. . . . . . . 8
β’ ((πβπ₯) /π π΄) β V |
3 | 2 | rgenw 3065 |
. . . . . . 7
β’
βπ₯ β
π ((πβπ₯) /π π΄) β V |
4 | | dmmptg 6198 |
. . . . . . 7
β’
(βπ₯ β
π ((πβπ₯) /π π΄) β V β dom (π₯ β π β¦ ((πβπ₯) /π π΄)) = π) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
β’ dom
(π₯ β π β¦ ((πβπ₯) /π π΄)) = π |
6 | | df-fn 6503 |
. . . . . 6
β’ ((π₯ β π β¦ ((πβπ₯) /π π΄)) Fn π β (Fun (π₯ β π β¦ ((πβπ₯) /π π΄)) β§ dom (π₯ β π β¦ ((πβπ₯) /π π΄)) = π)) |
7 | 1, 5, 6 | mpbir2an 710 |
. . . . 5
β’ (π₯ β π β¦ ((πβπ₯) /π π΄)) Fn π |
8 | 7 | a1i 11 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π₯ β π β¦ ((πβπ₯) /π π΄)) Fn π) |
9 | | vex 3451 |
. . . . . . 7
β’ π¦ β V |
10 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β π β¦ ((πβπ₯) /π π΄)) = (π₯ β π β¦ ((πβπ₯) /π π΄)) |
11 | 10 | elrnmpt 5915 |
. . . . . . 7
β’ (π¦ β V β (π¦ β ran (π₯ β π β¦ ((πβπ₯) /π π΄)) β βπ₯ β π π¦ = ((πβπ₯) /π π΄))) |
12 | 9, 11 | ax-mp 5 |
. . . . . 6
β’ (π¦ β ran (π₯ β π β¦ ((πβπ₯) /π π΄)) β βπ₯ β π π¦ = ((πβπ₯) /π π΄)) |
13 | | measfrge0 32866 |
. . . . . . . . . . 11
β’ (π β (measuresβπ) β π:πβΆ(0[,]+β)) |
14 | | ffvelcdm 7036 |
. . . . . . . . . . 11
β’ ((π:πβΆ(0[,]+β) β§ π₯ β π) β (πβπ₯) β (0[,]+β)) |
15 | 13, 14 | sylan 581 |
. . . . . . . . . 10
β’ ((π β (measuresβπ) β§ π₯ β π) β (πβπ₯) β (0[,]+β)) |
16 | 15 | adantlr 714 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π₯ β π) β (πβπ₯) β (0[,]+β)) |
17 | | simplr 768 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π₯ β π) β π΄ β
β+) |
18 | 16, 17 | xrpxdivcld 31847 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π₯ β π) β ((πβπ₯) /π π΄) β (0[,]+β)) |
19 | | eleq1a 2829 |
. . . . . . . 8
β’ (((πβπ₯) /π π΄) β (0[,]+β) β (π¦ = ((πβπ₯) /π π΄) β π¦ β (0[,]+β))) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π₯ β π) β (π¦ = ((πβπ₯) /π π΄) β π¦ β (0[,]+β))) |
21 | 20 | rexlimdva 3149 |
. . . . . 6
β’ ((π β (measuresβπ) β§ π΄ β β+) β
(βπ₯ β π π¦ = ((πβπ₯) /π π΄) β π¦ β (0[,]+β))) |
22 | 12, 21 | biimtrid 241 |
. . . . 5
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π¦ β ran (π₯ β π β¦ ((πβπ₯) /π π΄)) β π¦ β (0[,]+β))) |
23 | 22 | ssrdv 3954 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β β+) β ran
(π₯ β π β¦ ((πβπ₯) /π π΄)) β (0[,]+β)) |
24 | | df-f 6504 |
. . . 4
β’ ((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β ((π₯ β π β¦ ((πβπ₯) /π π΄)) Fn π β§ ran (π₯ β π β¦ ((πβπ₯) /π π΄)) β (0[,]+β))) |
25 | 8, 23, 24 | sylanbrc 584 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β)) |
26 | | measbase 32860 |
. . . . . . . 8
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
27 | | 0elsiga 32777 |
. . . . . . . 8
β’ (π β βͺ ran sigAlgebra β β
β π) |
28 | 26, 27 | syl 17 |
. . . . . . 7
β’ (π β (measuresβπ) β β
β π) |
29 | 28 | adantr 482 |
. . . . . 6
β’ ((π β (measuresβπ) β§ π΄ β β+) β β
β π) |
30 | | ovex 7394 |
. . . . . 6
β’ ((πββ
)
/π π΄)
β V |
31 | 29, 30 | jctir 522 |
. . . . 5
β’ ((π β (measuresβπ) β§ π΄ β β+) β (β
β π β§ ((πββ
)
/π π΄)
β V)) |
32 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = β
β (πβπ₯) = (πββ
)) |
33 | 32 | oveq1d 7376 |
. . . . . 6
β’ (π₯ = β
β ((πβπ₯) /π π΄) = ((πββ
) /π π΄)) |
34 | 33, 10 | fvmptg 6950 |
. . . . 5
β’ ((β
β π β§ ((πββ
)
/π π΄)
β V) β ((π₯ β
π β¦ ((πβπ₯) /π π΄))ββ
) = ((πββ
) /π π΄)) |
35 | 31, 34 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β β+) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = ((πββ
) /π π΄)) |
36 | | measvnul 32869 |
. . . . . 6
β’ (π β (measuresβπ) β (πββ
) = 0) |
37 | 36 | oveq1d 7376 |
. . . . 5
β’ (π β (measuresβπ) β ((πββ
) /π π΄) = (0 /π
π΄)) |
38 | | xdiv0rp 31842 |
. . . . 5
β’ (π΄ β β+
β (0 /π π΄) = 0) |
39 | 37, 38 | sylan9eq 2793 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β β+) β ((πββ
)
/π π΄) =
0) |
40 | 35, 39 | eqtrd 2773 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0) |
41 | | simpll 766 |
. . . . . 6
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (π β (measuresβπ) β§ π΄ β
β+)) |
42 | | simplr 768 |
. . . . . . 7
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π¦ β π« π) |
43 | | simprl 770 |
. . . . . . 7
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π¦ βΌ Ο) |
44 | | simprr 772 |
. . . . . . 7
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β Disj π§ β π¦ π§) |
45 | 42, 43, 44 | 3jca 1129 |
. . . . . 6
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) |
46 | 9 | a1i 11 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β π¦ β V) |
47 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ π§ β π¦) β π β (measuresβπ)) |
48 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ π§ β π¦) β π¦ β π« π) |
49 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ π§ β π¦) β π§ β π¦) |
50 | | elpwg 4567 |
. . . . . . . . . . . . 13
β’ (π¦ β V β (π¦ β π« π β π¦ β π)) |
51 | 9, 50 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (π¦ β π« π β π¦ β π) |
52 | | ssel2 3943 |
. . . . . . . . . . . 12
β’ ((π¦ β π β§ π§ β π¦) β π§ β π) |
53 | 51, 52 | sylanb 582 |
. . . . . . . . . . 11
β’ ((π¦ β π« π β§ π§ β π¦) β π§ β π) |
54 | 48, 49, 53 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ π§ β π¦) β π§ β π) |
55 | | measvxrge0 32868 |
. . . . . . . . . 10
β’ ((π β (measuresβπ) β§ π§ β π) β (πβπ§) β (0[,]+β)) |
56 | 47, 54, 55 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ π§ β π¦) β (πβπ§) β (0[,]+β)) |
57 | | simplr 768 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β π΄ β
β+) |
58 | 46, 56, 57 | esumdivc 32746 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β
(Ξ£*π§
β π¦(πβπ§) /π π΄) = Ξ£*π§ β π¦((πβπ§) /π π΄)) |
59 | 58 | 3ad2antr1 1189 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (Ξ£*π§ β π¦(πβπ§) /π π΄) = Ξ£*π§ β π¦((πβπ§) /π π΄)) |
60 | 26 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π β βͺ ran
sigAlgebra) |
61 | | simpr1 1195 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π¦ β π« π) |
62 | | simpr2 1196 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π¦ βΌ Ο) |
63 | | sigaclcu 32780 |
. . . . . . . . . 10
β’ ((π β βͺ ran sigAlgebra β§ π¦ β π« π β§ π¦ βΌ Ο) β βͺ π¦
β π) |
64 | 60, 61, 62, 63 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β βͺ π¦ β π) |
65 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π₯ = βͺ
π¦ β (πβπ₯) = (πββͺ π¦)) |
66 | 65 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π₯ = βͺ
π¦ β ((πβπ₯) /π π΄) = ((πββͺ π¦) /π π΄)) |
67 | 66, 10, 2 | fvmpt3i 6957 |
. . . . . . . . 9
β’ (βͺ π¦
β π β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = ((πββͺ π¦) /π π΄)) |
68 | 64, 67 | syl 17 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = ((πββͺ π¦) /π π΄)) |
69 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β π β (measuresβπ)) |
70 | 69, 61 | jca 513 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (π β (measuresβπ) β§ π¦ β π« π)) |
71 | | simpr3 1197 |
. . . . . . . . . . 11
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β Disj π§ β π¦ π§) |
72 | 62, 71 | jca 513 |
. . . . . . . . . 10
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) |
73 | | measvun 32872 |
. . . . . . . . . . . . 13
β’ ((π β (measuresβπ) β§ π¦ β π« π β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (πββͺ π¦) = Ξ£*π§ β π¦(πβπ§)) |
74 | 73 | 3expia 1122 |
. . . . . . . . . . . 12
β’ ((π β (measuresβπ) β§ π¦ β π« π) β ((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β (πββͺ π¦) = Ξ£*π§ β π¦(πβπ§))) |
75 | 74 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β (measuresβπ) β βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β (πββͺ π¦) = Ξ£*π§ β π¦(πβπ§))) |
76 | 75 | r19.21bi 3233 |
. . . . . . . . . 10
β’ ((π β (measuresβπ) β§ π¦ β π« π) β ((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β (πββͺ π¦) = Ξ£*π§ β π¦(πβπ§))) |
77 | 70, 72, 76 | sylc 65 |
. . . . . . . . 9
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β (πββͺ π¦) = Ξ£*π§ β π¦(πβπ§)) |
78 | 77 | oveq1d 7376 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((πββͺ π¦) /π π΄) = (Ξ£*π§ β π¦(πβπ§) /π π΄)) |
79 | 68, 78 | eqtrd 2773 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = (Ξ£*π§ β π¦(πβπ§) /π π΄)) |
80 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (πβπ₯) = (πβπ§)) |
81 | 80 | oveq1d 7376 |
. . . . . . . . . . 11
β’ (π₯ = π§ β ((πβπ₯) /π π΄) = ((πβπ§) /π π΄)) |
82 | 81, 10, 2 | fvmpt3i 6957 |
. . . . . . . . . 10
β’ (π§ β π β ((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§) = ((πβπ§) /π π΄)) |
83 | 53, 82 | syl 17 |
. . . . . . . . 9
β’ ((π¦ β π« π β§ π§ β π¦) β ((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§) = ((πβπ§) /π π΄)) |
84 | 83 | esumeq2dv 32701 |
. . . . . . . 8
β’ (π¦ β π« π β Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§) = Ξ£*π§ β π¦((πβπ§) /π π΄)) |
85 | 61, 84 | syl 17 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§) = Ξ£*π§ β π¦((πβπ§) /π π΄)) |
86 | 59, 79, 85 | 3eqtr4d 2783 |
. . . . . 6
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ (π¦ β π« π β§ π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§)) |
87 | 41, 45, 86 | syl2anc 585 |
. . . . 5
β’ ((((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β§ (π¦ βΌ Ο β§ Disj π§ β π¦ π§)) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§)) |
88 | 87 | ex 414 |
. . . 4
β’ (((π β (measuresβπ) β§ π΄ β β+) β§ π¦ β π« π) β ((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))) |
89 | 88 | ralrimiva 3140 |
. . 3
β’ ((π β (measuresβπ) β§ π΄ β β+) β
βπ¦ β π«
π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))) |
90 | 25, 40, 89 | 3jca 1129 |
. 2
β’ ((π β (measuresβπ) β§ π΄ β β+) β ((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§)))) |
91 | | ismeas 32862 |
. . . . 5
β’ (π β βͺ ran sigAlgebra β ((π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ) β ((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))))) |
92 | 26, 91 | syl 17 |
. . . 4
β’ (π β (measuresβπ) β ((π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ) β ((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))))) |
93 | 92 | biimprd 248 |
. . 3
β’ (π β (measuresβπ) β (((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))) β (π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ))) |
94 | 93 | adantr 482 |
. 2
β’ ((π β (measuresβπ) β§ π΄ β β+) β (((π₯ β π β¦ ((πβπ₯) /π π΄)):πβΆ(0[,]+β) β§ ((π₯ β π β¦ ((πβπ₯) /π π΄))ββ
) = 0 β§ βπ¦ β π« π((π¦ βΌ Ο β§ Disj π§ β π¦ π§) β ((π₯ β π β¦ ((πβπ₯) /π π΄))ββͺ π¦) = Ξ£*π§ β π¦((π₯ β π β¦ ((πβπ₯) /π π΄))βπ§))) β (π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ))) |
95 | 90, 94 | mpd 15 |
1
β’ ((π β (measuresβπ) β§ π΄ β β+) β (π₯ β π β¦ ((πβπ₯) /π π΄)) β (measuresβπ)) |