Step | Hyp | Ref
| Expression |
1 | | caratheodorylem2.o |
. . 3
β’ (π β π β OutMeas) |
2 | | caratheodorylem2.x |
. . 3
β’ π = βͺ
dom π |
3 | | caratheodorylem2.s |
. . . . . . . . . . 11
β’ π = (CaraGenβπ) |
4 | 3 | caragenss 45220 |
. . . . . . . . . 10
β’ (π β OutMeas β π β dom π) |
5 | 1, 4 | syl 17 |
. . . . . . . . 9
β’ (π β π β dom π) |
6 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π β dom π) |
7 | | caratheodorylem2.e |
. . . . . . . . 9
β’ (π β πΈ:ββΆπ) |
8 | 7 | ffvelcdmda 7087 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΈβπ) β π) |
9 | 6, 8 | sseldd 3984 |
. . . . . . 7
β’ ((π β§ π β β) β (πΈβπ) β dom π) |
10 | | elssuni 4942 |
. . . . . . 7
β’ ((πΈβπ) β dom π β (πΈβπ) β βͺ dom
π) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β (πΈβπ) β βͺ dom
π) |
12 | 11, 2 | sseqtrrdi 4034 |
. . . . 5
β’ ((π β§ π β β) β (πΈβπ) β π) |
13 | 12 | ralrimiva 3147 |
. . . 4
β’ (π β βπ β β (πΈβπ) β π) |
14 | | iunss 5049 |
. . . 4
β’ (βͺ π β β (πΈβπ) β π β βπ β β (πΈβπ) β π) |
15 | 13, 14 | sylibr 233 |
. . 3
β’ (π β βͺ π β β (πΈβπ) β π) |
16 | 1, 2, 15 | omexrcl 45223 |
. 2
β’ (π β (πββͺ
π β β (πΈβπ)) β
β*) |
17 | | nnex 12218 |
. . . 4
β’ β
β V |
18 | 17 | a1i 11 |
. . 3
β’ (π β β β
V) |
19 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π β OutMeas) |
20 | 19, 2, 12 | omecl 45219 |
. . . 4
β’ ((π β§ π β β) β (πβ(πΈβπ)) β (0[,]+β)) |
21 | | eqid 2733 |
. . . 4
β’ (π β β β¦ (πβ(πΈβπ))) = (π β β β¦ (πβ(πΈβπ))) |
22 | 20, 21 | fmptd 7114 |
. . 3
β’ (π β (π β β β¦ (πβ(πΈβπ))):ββΆ(0[,]+β)) |
23 | 18, 22 | sge0xrcl 45101 |
. 2
β’ (π β
(Ξ£^β(π β β β¦ (πβ(πΈβπ)))) β
β*) |
24 | | nfv 1918 |
. . 3
β’
β²ππ |
25 | | nfcv 2904 |
. . 3
β’
β²ππΈ |
26 | | nnuz 12865 |
. . 3
β’ β =
(β€β₯β1) |
27 | 1, 2, 3 | caragensspw 45225 |
. . . 4
β’ (π β π β π« π) |
28 | 7, 27 | fssd 6736 |
. . 3
β’ (π β πΈ:ββΆπ« π) |
29 | 24, 25, 1, 2, 26, 28 | omeiunle 45233 |
. 2
β’ (π β (πββͺ
π β β (πΈβπ)) β€
(Ξ£^β(π β β β¦ (πβ(πΈβπ))))) |
30 | | elpwinss 43736 |
. . . . . . . 8
β’ (π₯ β (π« β β©
Fin) β π₯ β
β) |
31 | 30 | resmptd 6041 |
. . . . . . 7
β’ (π₯ β (π« β β©
Fin) β ((π β
β β¦ (πβ(πΈβπ))) βΎ π₯) = (π β π₯ β¦ (πβ(πΈβπ)))) |
32 | 31 | fveq2d 6896 |
. . . . . 6
β’ (π₯ β (π« β β©
Fin) β (Ξ£^β((π β β β¦ (πβ(πΈβπ))) βΎ π₯)) =
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ))))) |
33 | 32 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β (π« β β© Fin)) β
(Ξ£^β((π β β β¦ (πβ(πΈβπ))) βΎ π₯)) =
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ))))) |
34 | | 1zzd 12593 |
. . . . . . 7
β’ ((π β§ π₯ β (π« β β© Fin)) β
1 β β€) |
35 | 30 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β (π« β β© Fin)) β
π₯ β
β) |
36 | | elinel2 4197 |
. . . . . . . 8
β’ (π₯ β (π« β β©
Fin) β π₯ β
Fin) |
37 | 36 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β (π« β β© Fin)) β
π₯ β
Fin) |
38 | 34, 26, 35, 37 | uzfissfz 44036 |
. . . . . 6
β’ ((π β§ π₯ β (π« β β© Fin)) β
βπ β β
π₯ β (1...π)) |
39 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π₯ β V |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...π)) β π₯ β V) |
41 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1...π)) β§ π β π₯) β π β OutMeas) |
42 | 28 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1...π)) β§ π β π₯) β πΈ:ββΆπ« π) |
43 | | fz1ssnn 13532 |
. . . . . . . . . . . . . . . . . 18
β’
(1...π) β
β |
44 | | ssel2 3978 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (1...π) β§ π β π₯) β π β (1...π)) |
45 | 43, 44 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β (1...π) β§ π β π₯) β π β β) |
46 | 45 | adantll 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1...π)) β§ π β π₯) β π β β) |
47 | 42, 46 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1...π)) β§ π β π₯) β (πΈβπ) β π« π) |
48 | | elpwi 4610 |
. . . . . . . . . . . . . . 15
β’ ((πΈβπ) β π« π β (πΈβπ) β π) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1...π)) β§ π β π₯) β (πΈβπ) β π) |
50 | 41, 2, 49 | omecl 45219 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1...π)) β§ π β π₯) β (πβ(πΈβπ)) β (0[,]+β)) |
51 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π β π₯ β¦ (πβ(πΈβπ))) = (π β π₯ β¦ (πβ(πΈβπ))) |
52 | 50, 51 | fmptd 7114 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...π)) β (π β π₯ β¦ (πβ(πΈβπ))):π₯βΆ(0[,]+β)) |
53 | 40, 52 | sge0xrcl 45101 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...π)) β
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ)))) β
β*) |
54 | 53 | 3adant2 1132 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ π₯ β (1...π)) β
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ)))) β
β*) |
55 | | ovex 7442 |
. . . . . . . . . . . . 13
β’
(1...π) β
V |
56 | 55 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (1...π) β V) |
57 | | elfznn 13530 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β π β β) |
58 | 57, 20 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πβ(πΈβπ)) β (0[,]+β)) |
59 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β¦ (πβ(πΈβπ))) = (π β (1...π) β¦ (πβ(πΈβπ))) |
60 | 58, 59 | fmptd 7114 |
. . . . . . . . . . . 12
β’ (π β (π β (1...π) β¦ (πβ(πΈβπ))):(1...π)βΆ(0[,]+β)) |
61 | 56, 60 | sge0xrcl 45101 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β (1...π) β¦ (πβ(πΈβπ)))) β
β*) |
62 | 61 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ π₯ β (1...π)) β
(Ξ£^β(π β (1...π) β¦ (πβ(πΈβπ)))) β
β*) |
63 | 16 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ π₯ β (1...π)) β (πββͺ
π β β (πΈβπ)) β
β*) |
64 | 55 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β β§ π₯ β (1...π)) β (1...π) β V) |
65 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π β§ π β β β§ π₯ β (1...π)) β§ π β (1...π)) β π) |
66 | 57 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β β β§ π₯ β (1...π)) β§ π β (1...π)) β π β β) |
67 | 65, 66, 20 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π β β β§ π₯ β (1...π)) β§ π β (1...π)) β (πβ(πΈβπ)) β (0[,]+β)) |
68 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π β§ π β β β§ π₯ β (1...π)) β π₯ β (1...π)) |
69 | 64, 67, 68 | sge0lessmpt 45115 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ π₯ β (1...π)) β
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ)))) β€
(Ξ£^β(π β (1...π) β¦ (πβ(πΈβπ))))) |
70 | 1 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β OutMeas) |
71 | 7 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β πΈ:ββΆπ) |
72 | | caratheodorylem2.5 |
. . . . . . . . . . . . . . 15
β’ (π β Disj π β β (πΈβπ)) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β Disj π β β (πΈβπ)) |
74 | | caratheodorylem2.g |
. . . . . . . . . . . . . . 15
β’ πΊ = (π β β β¦ βͺ π β (1...π)(πΈβπ)) |
75 | | nfiu1 5032 |
. . . . . . . . . . . . . . . 16
β’
β²πβͺ π β (1...π)(πΈβπ) |
76 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²πβͺ π β (1...π)(πΈβπ) |
77 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΈβπ) = (πΈβπ)) |
78 | 77 | cbviunv 5044 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π β (1...π)(πΈβπ) = βͺ π β (1...π)(πΈβπ) |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β βͺ
π β (1...π)(πΈβπ) = βͺ π β (1...π)(πΈβπ)) |
80 | | oveq2 7417 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (1...π) = (1...π)) |
81 | 80 | iuneq1d 5025 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β βͺ
π β (1...π)(πΈβπ) = βͺ π β (1...π)(πΈβπ)) |
82 | 79, 81 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (π = π β βͺ
π β (1...π)(πΈβπ) = βͺ π β (1...π)(πΈβπ)) |
83 | 75, 76, 82 | cbvmpt 5260 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ βͺ π β (1...π)(πΈβπ)) = (π β β β¦ βͺ π β (1...π)(πΈβπ)) |
84 | 74, 83 | eqtri 2761 |
. . . . . . . . . . . . . 14
β’ πΊ = (π β β β¦ βͺ π β (1...π)(πΈβπ)) |
85 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
86 | 85, 26 | eleqtrdi 2844 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
(β€β₯β1)) |
87 | 86 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
88 | 70, 3, 26, 71, 73, 84, 87 | caratheodorylem1 45242 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβ(πΊβπ)) =
(Ξ£^β(π β (1...π) β¦ (πβ(πΈβπ))))) |
89 | 88 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β
(Ξ£^β(π β (1...π) β¦ (πβ(πΈβπ)))) = (πβ(πΊβπ))) |
90 | 15 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β βͺ π β β (πΈβπ) β π) |
91 | | fvex 6905 |
. . . . . . . . . . . . . . . . 17
β’ (πΈβπ) β V |
92 | 55, 91 | iunex 7955 |
. . . . . . . . . . . . . . . 16
β’ βͺ π β (1...π)(πΈβπ) β V |
93 | 74 | fvmpt2 7010 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ βͺ π β (1...π)(πΈβπ) β V) β (πΊβπ) = βͺ π β (1...π)(πΈβπ)) |
94 | 85, 92, 93 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β β β (πΊβπ) = βͺ π β (1...π)(πΈβπ)) |
95 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(1...π) β
β) |
96 | | iunss1 5012 |
. . . . . . . . . . . . . . . 16
β’
((1...π) β
β β βͺ π β (1...π)(πΈβπ) β βͺ
π β β (πΈβπ)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β β β βͺ π β (1...π)(πΈβπ) β βͺ
π β β (πΈβπ)) |
98 | 94, 97 | eqsstrd 4021 |
. . . . . . . . . . . . . 14
β’ (π β β β (πΊβπ) β βͺ
π β β (πΈβπ)) |
99 | 98 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΊβπ) β βͺ
π β β (πΈβπ)) |
100 | 70, 2, 90, 99 | omessle 45214 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβ(πΊβπ)) β€ (πββͺ
π β β (πΈβπ))) |
101 | 89, 100 | eqbrtrd 5171 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β
(Ξ£^β(π β (1...π) β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ))) |
102 | 101 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ π₯ β (1...π)) β
(Ξ£^β(π β (1...π) β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ))) |
103 | 54, 62, 63, 69, 102 | xrletrd 13141 |
. . . . . . . . 9
β’ ((π β§ π β β β§ π₯ β (1...π)) β
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ))) |
104 | 103 | 3exp 1120 |
. . . . . . . 8
β’ (π β (π β β β (π₯ β (1...π) β
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ))))) |
105 | 104 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (π« β β© Fin)) β
(π β β β
(π₯ β (1...π) β
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ))))) |
106 | 105 | rexlimdv 3154 |
. . . . . 6
β’ ((π β§ π₯ β (π« β β© Fin)) β
(βπ β β
π₯ β (1...π) β
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ)))) |
107 | 38, 106 | mpd 15 |
. . . . 5
β’ ((π β§ π₯ β (π« β β© Fin)) β
(Ξ£^β(π β π₯ β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ))) |
108 | 33, 107 | eqbrtrd 5171 |
. . . 4
β’ ((π β§ π₯ β (π« β β© Fin)) β
(Ξ£^β((π β β β¦ (πβ(πΈβπ))) βΎ π₯)) β€ (πββͺ
π β β (πΈβπ))) |
109 | 108 | ralrimiva 3147 |
. . 3
β’ (π β βπ₯ β (π« β β©
Fin)(Ξ£^β((π β β β¦ (πβ(πΈβπ))) βΎ π₯)) β€ (πββͺ
π β β (πΈβπ))) |
110 | 18, 22, 16 | sge0lefi 45114 |
. . 3
β’ (π β
((Ξ£^β(π β β β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ)) β βπ₯ β (π« β β©
Fin)(Ξ£^β((π β β β¦ (πβ(πΈβπ))) βΎ π₯)) β€ (πββͺ
π β β (πΈβπ)))) |
111 | 109, 110 | mpbird 257 |
. 2
β’ (π β
(Ξ£^β(π β β β¦ (πβ(πΈβπ)))) β€ (πββͺ
π β β (πΈβπ))) |
112 | 16, 23, 29, 111 | xrletrid 13134 |
1
β’ (π β (πββͺ
π β β (πΈβπ)) =
(Ξ£^β(π β β β¦ (πβ(πΈβπ))))) |