Step | Hyp | Ref
| Expression |
1 | | iccssxr 13410 |
. . 3
β’
(0[,]+β) β β* |
2 | | measiun.1 |
. . . 4
β’ (π β π β (measuresβπ)) |
3 | | measiun.2 |
. . . 4
β’ (π β π΄ β π) |
4 | | measvxrge0 33732 |
. . . 4
β’ ((π β (measuresβπ) β§ π΄ β π) β (πβπ΄) β (0[,]+β)) |
5 | 2, 3, 4 | syl2anc 583 |
. . 3
β’ (π β (πβπ΄) β (0[,]+β)) |
6 | 1, 5 | sselid 3975 |
. 2
β’ (π β (πβπ΄) β
β*) |
7 | | measbase 33724 |
. . . . . 6
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
8 | 2, 7 | syl 17 |
. . . . 5
β’ (π β π β βͺ ran
sigAlgebra) |
9 | | measiun.3 |
. . . . . 6
β’ ((π β§ π β β) β π΅ β π) |
10 | 9 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β β π΅ β π) |
11 | | sigaclcu2 33647 |
. . . . 5
β’ ((π β βͺ ran sigAlgebra β§ βπ β β π΅ β π) β βͺ
π β β π΅ β π) |
12 | 8, 10, 11 | syl2anc 583 |
. . . 4
β’ (π β βͺ π β β π΅ β π) |
13 | | measvxrge0 33732 |
. . . 4
β’ ((π β (measuresβπ) β§ βͺ π β β π΅ β π) β (πββͺ
π β β π΅) β
(0[,]+β)) |
14 | 2, 12, 13 | syl2anc 583 |
. . 3
β’ (π β (πββͺ
π β β π΅) β
(0[,]+β)) |
15 | 1, 14 | sselid 3975 |
. 2
β’ (π β (πββͺ
π β β π΅) β
β*) |
16 | | nnex 12219 |
. . . 4
β’ β
β V |
17 | 2 | adantr 480 |
. . . . . 6
β’ ((π β§ π β β) β π β (measuresβπ)) |
18 | | measvxrge0 33732 |
. . . . . 6
β’ ((π β (measuresβπ) β§ π΅ β π) β (πβπ΅) β (0[,]+β)) |
19 | 17, 9, 18 | syl2anc 583 |
. . . . 5
β’ ((π β§ π β β) β (πβπ΅) β (0[,]+β)) |
20 | 19 | ralrimiva 3140 |
. . . 4
β’ (π β βπ β β (πβπ΅) β (0[,]+β)) |
21 | | nfcv 2897 |
. . . . 5
β’
β²πβ |
22 | 21 | esumcl 33557 |
. . . 4
β’ ((β
β V β§ βπ
β β (πβπ΅) β (0[,]+β)) β
Ξ£*π β
β(πβπ΅) β
(0[,]+β)) |
23 | 16, 20, 22 | sylancr 586 |
. . 3
β’ (π β Ξ£*π β β(πβπ΅) β (0[,]+β)) |
24 | 1, 23 | sselid 3975 |
. 2
β’ (π β Ξ£*π β β(πβπ΅) β
β*) |
25 | | measiun.4 |
. . 3
β’ (π β π΄ β βͺ
π β β π΅) |
26 | 2, 3, 12, 25 | measssd 33742 |
. 2
β’ (π β (πβπ΄) β€ (πββͺ
π β β π΅)) |
27 | | nfcsb1v 3913 |
. . . 4
β’
β²πβ¦π / πβ¦π΅ |
28 | | csbeq1a 3902 |
. . . 4
β’ (π = π β π΅ = β¦π / πβ¦π΅) |
29 | | eqidd 2727 |
. . . . 5
β’ (π β β =
β) |
30 | 29 | orcd 870 |
. . . 4
β’ (π β (β = β β¨
β = (1..^π))) |
31 | 27, 28, 30, 2, 9 | measiuns 33744 |
. . 3
β’ (π β (πββͺ
π β β π΅) = Ξ£*π β β(πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅))) |
32 | 16 | a1i 11 |
. . . 4
β’ (π β β β
V) |
33 | 8 | adantr 480 |
. . . . . 6
β’ ((π β§ π β β) β π β βͺ ran
sigAlgebra) |
34 | | nfv 1909 |
. . . . . . . . . . 11
β’
β²ππ |
35 | | nfcv 2897 |
. . . . . . . . . . . . 13
β’
β²ππ |
36 | 35 | nfel1 2913 |
. . . . . . . . . . . 12
β’
β²π π β β |
37 | 27 | nfel1 2913 |
. . . . . . . . . . . 12
β’
β²πβ¦π / πβ¦π΅ β π |
38 | 36, 37 | nfim 1891 |
. . . . . . . . . . 11
β’
β²π(π β β β
β¦π / πβ¦π΅ β π) |
39 | 34, 38 | nfim 1891 |
. . . . . . . . . 10
β’
β²π(π β (π β β β β¦π / πβ¦π΅ β π)) |
40 | | eleq1w 2810 |
. . . . . . . . . . . 12
β’ (π = π β (π β β β π β β)) |
41 | 28 | eleq1d 2812 |
. . . . . . . . . . . 12
β’ (π = π β (π΅ β π β β¦π / πβ¦π΅ β π)) |
42 | 40, 41 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π = π β ((π β β β π΅ β π) β (π β β β β¦π / πβ¦π΅ β π))) |
43 | 42 | imbi2d 340 |
. . . . . . . . . 10
β’ (π = π β ((π β (π β β β π΅ β π)) β (π β (π β β β β¦π / πβ¦π΅ β π)))) |
44 | 9 | ex 412 |
. . . . . . . . . 10
β’ (π β (π β β β π΅ β π)) |
45 | 39, 43, 44 | chvarfv 2225 |
. . . . . . . . 9
β’ (π β (π β β β β¦π / πβ¦π΅ β π)) |
46 | 45 | ralrimiv 3139 |
. . . . . . . 8
β’ (π β βπ β β β¦π / πβ¦π΅ β π) |
47 | | fzossnn 13684 |
. . . . . . . . . 10
β’
(1..^π) β
β |
48 | | ssralv 4045 |
. . . . . . . . . 10
β’
((1..^π) β
β β (βπ
β β β¦π / πβ¦π΅ β π β βπ β (1..^π)β¦π / πβ¦π΅ β π)) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ β
β β¦π /
πβ¦π΅ β π β βπ β (1..^π)β¦π / πβ¦π΅ β π) |
50 | | sigaclfu2 33648 |
. . . . . . . . 9
β’ ((π β βͺ ran sigAlgebra β§ βπ β (1..^π)β¦π / πβ¦π΅ β π) β βͺ
π β (1..^π)β¦π / πβ¦π΅ β π) |
51 | 49, 50 | sylan2 592 |
. . . . . . . 8
β’ ((π β βͺ ran sigAlgebra β§ βπ β β β¦π / πβ¦π΅ β π) β βͺ
π β (1..^π)β¦π / πβ¦π΅ β π) |
52 | 8, 46, 51 | syl2anc 583 |
. . . . . . 7
β’ (π β βͺ π β (1..^π)β¦π / πβ¦π΅ β π) |
53 | 52 | adantr 480 |
. . . . . 6
β’ ((π β§ π β β) β βͺ π β (1..^π)β¦π / πβ¦π΅ β π) |
54 | | difelsiga 33660 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π΅ β π β§ βͺ
π β (1..^π)β¦π / πβ¦π΅ β π) β (π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅) β π) |
55 | 33, 9, 53, 54 | syl3anc 1368 |
. . . . 5
β’ ((π β§ π β β) β (π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅) β π) |
56 | | measvxrge0 33732 |
. . . . 5
β’ ((π β (measuresβπ) β§ (π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅) β π) β (πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅)) β (0[,]+β)) |
57 | 17, 55, 56 | syl2anc 583 |
. . . 4
β’ ((π β§ π β β) β (πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅)) β (0[,]+β)) |
58 | | difssd 4127 |
. . . . 5
β’ ((π β§ π β β) β (π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅) β π΅) |
59 | 17, 55, 9, 58 | measssd 33742 |
. . . 4
β’ ((π β§ π β β) β (πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅)) β€ (πβπ΅)) |
60 | 32, 57, 19, 59 | esumle 33585 |
. . 3
β’ (π β Ξ£*π β β(πβ(π΅ β βͺ
π β (1..^π)β¦π / πβ¦π΅)) β€ Ξ£*π β β(πβπ΅)) |
61 | 31, 60 | eqbrtrd 5163 |
. 2
β’ (π β (πββͺ
π β β π΅) β€ Ξ£*π β β(πβπ΅)) |
62 | 6, 15, 24, 26, 61 | xrletrd 13144 |
1
β’ (π β (πβπ΄) β€ Ξ£*π β β(πβπ΅)) |