Step | Hyp | Ref
| Expression |
1 | | iccssxr 13354 |
. . 3
β’
(0[,]+β) β β* |
2 | | measiun.1 |
. . . 4
β’ (π β π β (measuresβπ)) |
3 | | measiun.2 |
. . . 4
β’ (π β π΄ β π) |
4 | | measvxrge0 32844 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β π) β (πβπ΄) β (0[,]+β)) |
5 | 2, 3, 4 | syl2anc 585 |
. . 3
β’ (π β (πβπ΄) β (0[,]+β)) |
6 | 1, 5 | sselid 3947 |
. 2
β’ (π β (πβπ΄) β
β*) |
7 | | measbase 32836 |
. . . . . 6
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
8 | 2, 7 | syl 17 |
. . . . 5
β’ (π β π β βͺ ran
sigAlgebra) |
9 | | measiun.3 |
. . . . . 6
β’ ((π β§ π β β) β π΅ β π) |
10 | 9 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β β π΅ β π) |
11 | | sigaclcu2 32759 |
. . . . 5
β’ ((π β βͺ ran sigAlgebra β§ βπ β β π΅ β π) β βͺ
π β β π΅ β π) |
12 | 8, 10, 11 | syl2anc 585 |
. . . 4
β’ (π β βͺ π β β π΅ β π) |
13 | | measvxrge0 32844 |
. . . 4
β’ ((π β (measuresβπ) β§ βͺ π β β π΅ β π) β (πββͺ
π β β π΅) β
(0[,]+β)) |
14 | 2, 12, 13 | syl2anc 585 |
. . 3
β’ (π β (πββͺ
π β β π΅) β
(0[,]+β)) |
15 | 1, 14 | sselid 3947 |
. 2
β’ (π β (πββͺ
π β β π΅) β
β*) |
16 | | nnex 12166 |
. . . 4
β’ β
β V |
17 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π β (measuresβπ)) |
18 | | measvxrge0 32844 |
. . . . . 6
β’ ((π β (measuresβπ) β§ π΅ β π) β (πβπ΅) β (0[,]+β)) |
19 | 17, 9, 18 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β β) β (πβπ΅) β (0[,]+β)) |
20 | 19 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β β (πβπ΅) β (0[,]+β)) |
21 | | nfcv 2908 |
. . . . 5
β’
β²πβ |
22 | 21 | esumcl 32669 |
. . . 4
β’ ((β
β V β§ βπ
β β (πβπ΅) β (0[,]+β)) β
Ξ£*π β
β(πβπ΅) β
(0[,]+β)) |
23 | 16, 20, 22 | sylancr 588 |
. . 3
β’ (π β Ξ£*π β β(πβπ΅) β (0[,]+β)) |
24 | 1, 23 | sselid 3947 |
. 2
β’ (π β Ξ£*π β β(πβπ΅) β
β*) |
25 | | measiun.4 |
. . 3
β’ (π β π΄ β βͺ
π β β π΅) |
26 | 2, 3, 12, 25 | measssd 32854 |
. 2
β’ (π β (πβπ΄) β€ (πββͺ
π β β π΅)) |
27 | | nfcsb1v 3885 |
. . . 4
β’
β²πβ¦π / πβ¦π΅ |
28 | | csbeq1a 3874 |
. . . 4
β’ (π = π β π΅ = β¦π / πβ¦π΅) |
29 | | eqidd 2738 |
. . . . 5
β’ (π β β =
β) |
30 | 29 | orcd 872 |
. . . 4
β’ (π β (β = β β¨
β = (1..^π))) |
31 | 27, 28, 30, 2, 9 | measiuns 32856 |
. . 3
β’ (π β (πββͺ
π β β π΅) = Ξ£*π β β(πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅))) |
32 | 16 | a1i 11 |
. . . 4
β’ (π β β β
V) |
33 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π β βͺ ran
sigAlgebra) |
34 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²ππ |
35 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²ππ |
36 | 35 | nfel1 2924 |
. . . . . . . . . . . 12
β’
β²π π β β |
37 | 27 | nfel1 2924 |
. . . . . . . . . . . 12
β’
β²πβ¦π / πβ¦π΅ β π |
38 | 36, 37 | nfim 1900 |
. . . . . . . . . . 11
β’
β²π(π β β β
β¦π / πβ¦π΅ β π) |
39 | 34, 38 | nfim 1900 |
. . . . . . . . . 10
β’
β²π(π β (π β β β β¦π / πβ¦π΅ β π)) |
40 | | eleq1w 2821 |
. . . . . . . . . . . 12
β’ (π = π β (π β β β π β β)) |
41 | 28 | eleq1d 2823 |
. . . . . . . . . . . 12
β’ (π = π β (π΅ β π β β¦π / πβ¦π΅ β π)) |
42 | 40, 41 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β ((π β β β π΅ β π) β (π β β β β¦π / πβ¦π΅ β π))) |
43 | 42 | imbi2d 341 |
. . . . . . . . . 10
β’ (π = π β ((π β (π β β β π΅ β π)) β (π β (π β β β β¦π / πβ¦π΅ β π)))) |
44 | 9 | ex 414 |
. . . . . . . . . 10
β’ (π β (π β β β π΅ β π)) |
45 | 39, 43, 44 | chvarfv 2234 |
. . . . . . . . 9
β’ (π β (π β β β β¦π / πβ¦π΅ β π)) |
46 | 45 | ralrimiv 3143 |
. . . . . . . 8
β’ (π β βπ β β β¦π / πβ¦π΅ β π) |
47 | | fzossnn 13628 |
. . . . . . . . . 10
β’
(1..^π) β
β |
48 | | ssralv 4015 |
. . . . . . . . . 10
β’
((1..^π) β
β β (βπ
β β β¦π / πβ¦π΅ β π β βπ β (1..^π)β¦π / πβ¦π΅ β π)) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ β
β β¦π /
πβ¦π΅ β π β βπ β (1..^π)β¦π / πβ¦π΅ β π) |
50 | | sigaclfu2 32760 |
. . . . . . . . 9
β’ ((π β βͺ ran sigAlgebra β§ βπ β (1..^π)β¦π / πβ¦π΅ β π) β βͺ
π β (1..^π)β¦π / πβ¦π΅ β π) |
51 | 49, 50 | sylan2 594 |
. . . . . . . 8
β’ ((π β βͺ ran sigAlgebra β§ βπ β β β¦π / πβ¦π΅ β π) β βͺ
π β (1..^π)β¦π / πβ¦π΅ β π) |
52 | 8, 46, 51 | syl2anc 585 |
. . . . . . 7
β’ (π β βͺ π β (1..^π)β¦π / πβ¦π΅ β π) |
53 | 52 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β βͺ π β (1..^π)β¦π / πβ¦π΅ β π) |
54 | | difelsiga 32772 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π΅ β π β§ βͺ
π β (1..^π)β¦π / πβ¦π΅ β π) β (π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅) β π) |
55 | 33, 9, 53, 54 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β β) β (π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅) β π) |
56 | | measvxrge0 32844 |
. . . . 5
β’ ((π β (measuresβπ) β§ (π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅) β π) β (πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅)) β (0[,]+β)) |
57 | 17, 55, 56 | syl2anc 585 |
. . . 4
β’ ((π β§ π β β) β (πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅)) β (0[,]+β)) |
58 | | difssd 4097 |
. . . . 5
β’ ((π β§ π β β) β (π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅) β π΅) |
59 | 17, 55, 9, 58 | measssd 32854 |
. . . 4
β’ ((π β§ π β β) β (πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅)) β€ (πβπ΅)) |
60 | 32, 57, 19, 59 | esumle 32697 |
. . 3
β’ (π β Ξ£*π β β(πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅)) β€ Ξ£*π β β(πβπ΅)) |
61 | 31, 60 | eqbrtrd 5132 |
. 2
β’ (π β (πββͺ
π β β π΅) β€ Ξ£*π β β(πβπ΅)) |
62 | 6, 15, 24, 26, 61 | xrletrd 13088 |
1
β’ (π β (πβπ΄) β€ Ξ£*π β β(πβπ΅)) |