Step | Hyp | Ref
| Expression |
1 | | caratheodory.o |
. . 3
β’ (π β π β OutMeas) |
2 | | caratheodory.s |
. . 3
β’ π = (CaraGenβπ) |
3 | 1, 2 | caragensal 44840 |
. 2
β’ (π β π β SAlg) |
4 | | eqid 2737 |
. . . 4
β’ βͺ dom π = βͺ dom π |
5 | 1, 4 | omef 44811 |
. . 3
β’ (π β π:π« βͺ dom
πβΆ(0[,]+β)) |
6 | | caragenval 44808 |
. . . . . . 7
β’ (π β OutMeas β
(CaraGenβπ) = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
7 | 1, 6 | syl 17 |
. . . . . 6
β’ (π β (CaraGenβπ) = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
8 | 7 | eqcomd 2743 |
. . . . 5
β’ (π β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} = (CaraGenβπ)) |
9 | 2 | eqcomi 2746 |
. . . . . 6
β’
(CaraGenβπ) =
π |
10 | 9 | a1i 11 |
. . . . 5
β’ (π β (CaraGenβπ) = π) |
11 | 8, 10 | eqtr2d 2778 |
. . . 4
β’ (π β π = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
12 | | ssrab2 4042 |
. . . 4
β’ {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β π« βͺ dom π |
13 | 11, 12 | eqsstrdi 4003 |
. . 3
β’ (π β π β π« βͺ dom π) |
14 | 5, 13 | fssresd 6714 |
. 2
β’ (π β (π βΎ π):πβΆ(0[,]+β)) |
15 | 1, 2 | caragen0 44821 |
. . . 4
β’ (π β β
β π) |
16 | | fvres 6866 |
. . . 4
β’ (β
β π β ((π βΎ π)ββ
) = (πββ
)) |
17 | 15, 16 | syl 17 |
. . 3
β’ (π β ((π βΎ π)ββ
) = (πββ
)) |
18 | 1 | ome0 44812 |
. . 3
β’ (π β (πββ
) = 0) |
19 | 17, 18 | eqtrd 2777 |
. 2
β’ (π β ((π βΎ π)ββ
) = 0) |
20 | | simp1 1137 |
. . . 4
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β π) |
21 | | simp2 1138 |
. . . 4
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β π:ββΆπ) |
22 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
23 | 22 | cbvdisjv 5086 |
. . . . . 6
β’
(Disj π
β β (πβπ) β Disj π β β (πβπ)) |
24 | 23 | biimpi 215 |
. . . . 5
β’
(Disj π
β β (πβπ) β Disj π β β (πβπ)) |
25 | 24 | 3ad2ant3 1136 |
. . . 4
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β Disj π β β (πβπ)) |
26 | 1 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β π β OutMeas) |
27 | | simp2 1138 |
. . . . 5
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β π:ββΆπ) |
28 | 23 | biimpri 227 |
. . . . . 6
β’
(Disj π
β β (πβπ) β Disj π β β (πβπ)) |
29 | 28 | 3ad2ant3 1136 |
. . . . 5
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β Disj π β β (πβπ)) |
30 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
31 | 30 | cbviunv 5005 |
. . . . . 6
β’ βͺ π β (1...π)(πβπ) = βͺ π β (1...π)(πβπ) |
32 | 31 | mpteq2i 5215 |
. . . . 5
β’ (π β β β¦ βͺ π β (1...π)(πβπ)) = (π β β β¦ βͺ π β (1...π)(πβπ)) |
33 | 26, 4, 2, 27, 29, 32 | caratheodorylem2 44842 |
. . . 4
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β (πββͺ
π β β (πβπ)) =
(Ξ£^β(π β β β¦ (πβ(πβπ))))) |
34 | 20, 21, 25, 33 | syl3anc 1372 |
. . 3
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β (πββͺ
π β β (πβπ)) =
(Ξ£^β(π β β β¦ (πβ(πβπ))))) |
35 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π:ββΆπ) β π β SAlg) |
36 | | nnenom 13892 |
. . . . . . . 8
β’ β
β Ο |
37 | | endom 8926 |
. . . . . . . 8
β’ (β
β Ο β β βΌ Ο) |
38 | 36, 37 | ax-mp 5 |
. . . . . . 7
β’ β
βΌ Ο |
39 | 38 | a1i 11 |
. . . . . 6
β’ ((π β§ π:ββΆπ) β β βΌ
Ο) |
40 | | ffvelcdm 7037 |
. . . . . . 7
β’ ((π:ββΆπ β§ π β β) β (πβπ) β π) |
41 | 40 | adantll 713 |
. . . . . 6
β’ (((π β§ π:ββΆπ) β§ π β β) β (πβπ) β π) |
42 | 35, 39, 41 | saliuncl 44638 |
. . . . 5
β’ ((π β§ π:ββΆπ) β βͺ
π β β (πβπ) β π) |
43 | | fvres 6866 |
. . . . 5
β’ (βͺ π β β (πβπ) β π β ((π βΎ π)ββͺ
π β β (πβπ)) = (πββͺ
π β β (πβπ))) |
44 | 42, 43 | syl 17 |
. . . 4
β’ ((π β§ π:ββΆπ) β ((π βΎ π)ββͺ
π β β (πβπ)) = (πββͺ
π β β (πβπ))) |
45 | 44 | 3adant3 1133 |
. . 3
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β ((π βΎ π)ββͺ
π β β (πβπ)) = (πββͺ
π β β (πβπ))) |
46 | | fvres 6866 |
. . . . . . 7
β’ ((πβπ) β π β ((π βΎ π)β(πβπ)) = (πβ(πβπ))) |
47 | 41, 46 | syl 17 |
. . . . . 6
β’ (((π β§ π:ββΆπ) β§ π β β) β ((π βΎ π)β(πβπ)) = (πβ(πβπ))) |
48 | 47 | mpteq2dva 5210 |
. . . . 5
β’ ((π β§ π:ββΆπ) β (π β β β¦ ((π βΎ π)β(πβπ))) = (π β β β¦ (πβ(πβπ)))) |
49 | 48 | fveq2d 6851 |
. . . 4
β’ ((π β§ π:ββΆπ) β
(Ξ£^β(π β β β¦ ((π βΎ π)β(πβπ)))) =
(Ξ£^β(π β β β¦ (πβ(πβπ))))) |
50 | 49 | 3adant3 1133 |
. . 3
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β
(Ξ£^β(π β β β¦ ((π βΎ π)β(πβπ)))) =
(Ξ£^β(π β β β¦ (πβ(πβπ))))) |
51 | 34, 45, 50 | 3eqtr4d 2787 |
. 2
β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β ((π βΎ π)ββͺ
π β β (πβπ)) =
(Ξ£^β(π β β β¦ ((π βΎ π)β(πβπ))))) |
52 | 3, 14, 19, 51 | ismeannd 44782 |
1
β’ (π β (π βΎ π) β Meas) |