Step | Hyp | Ref
| Expression |
1 | | carageniuncl.o |
. 2
β’ (π β π β OutMeas) |
2 | | eqid 2737 |
. 2
β’ βͺ dom π = βͺ dom π |
3 | | carageniuncl.s |
. 2
β’ π = (CaraGenβπ) |
4 | | carageniuncl.e |
. . . . . . . 8
β’ (π β πΈ:πβΆπ) |
5 | 4 | ffvelcdmda 7040 |
. . . . . . 7
β’ ((π β§ π β π) β (πΈβπ) β π) |
6 | | elssuni 4903 |
. . . . . . 7
β’ ((πΈβπ) β π β (πΈβπ) β βͺ π) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ ((π β§ π β π) β (πΈβπ) β βͺ π) |
8 | 1, 3 | caragenuni 44826 |
. . . . . . 7
β’ (π β βͺ π =
βͺ dom π) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β βͺ π = βͺ
dom π) |
10 | 7, 9 | sseqtrd 3989 |
. . . . 5
β’ ((π β§ π β π) β (πΈβπ) β βͺ dom
π) |
11 | 10 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β π (πΈβπ) β βͺ dom
π) |
12 | | iunss 5010 |
. . . 4
β’ (βͺ π β π (πΈβπ) β βͺ dom
π β βπ β π (πΈβπ) β βͺ dom
π) |
13 | 11, 12 | sylibr 233 |
. . 3
β’ (π β βͺ π β π (πΈβπ) β βͺ dom
π) |
14 | | carageniuncl.z |
. . . . . . 7
β’ π =
(β€β₯βπ) |
15 | 14 | fvexi 6861 |
. . . . . 6
β’ π β V |
16 | | fvex 6860 |
. . . . . 6
β’ (πΈβπ) β V |
17 | 15, 16 | iunex 7906 |
. . . . 5
β’ βͺ π β π (πΈβπ) β V |
18 | 17 | a1i 11 |
. . . 4
β’ (π β βͺ π β π (πΈβπ) β V) |
19 | | elpwg 4568 |
. . . 4
β’ (βͺ π β π (πΈβπ) β V β (βͺ π β π (πΈβπ) β π« βͺ dom π β βͺ
π β π (πΈβπ) β βͺ dom
π)) |
20 | 18, 19 | syl 17 |
. . 3
β’ (π β (βͺ π β π (πΈβπ) β π« βͺ dom π β βͺ
π β π (πΈβπ) β βͺ dom
π)) |
21 | 13, 20 | mpbird 257 |
. 2
β’ (π β βͺ π β π (πΈβπ) β π« βͺ dom π) |
22 | | iccssxr 13354 |
. . . . 5
β’
(0[,]+β) β β* |
23 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β π β OutMeas) |
24 | | elpwi 4572 |
. . . . . . . 8
β’ (π β π« βͺ dom π β π β βͺ dom
π) |
25 | | ssinss1 4202 |
. . . . . . . 8
β’ (π β βͺ dom π β (π β© βͺ
π β π (πΈβπ)) β βͺ dom
π) |
26 | 24, 25 | syl 17 |
. . . . . . 7
β’ (π β π« βͺ dom π β (π β© βͺ
π β π (πΈβπ)) β βͺ dom
π) |
27 | 26 | adantl 483 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β (π β© βͺ
π β π (πΈβπ)) β βͺ dom
π) |
28 | 23, 2, 27 | omecl 44818 |
. . . . 5
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β© βͺ
π β π (πΈβπ))) β (0[,]+β)) |
29 | 22, 28 | sselid 3947 |
. . . 4
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β© βͺ
π β π (πΈβπ))) β
β*) |
30 | 24 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β π« βͺ dom π) β π β βͺ dom
π) |
31 | 30 | ssdifssd 4107 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β (π β βͺ
π β π (πΈβπ)) β βͺ dom
π) |
32 | 23, 2, 31 | omecl 44818 |
. . . . 5
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β βͺ
π β π (πΈβπ))) β (0[,]+β)) |
33 | 22, 32 | sselid 3947 |
. . . 4
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β βͺ
π β π (πΈβπ))) β
β*) |
34 | 29, 33 | xaddcld 13227 |
. . 3
β’ ((π β§ π β π« βͺ dom π) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β
β*) |
35 | 23, 2, 30 | omecl 44818 |
. . . 4
β’ ((π β§ π β π« βͺ dom π) β (πβπ) β (0[,]+β)) |
36 | 22, 35 | sselid 3947 |
. . 3
β’ ((π β§ π β π« βͺ dom π) β (πβπ) β
β*) |
37 | | pnfge 13058 |
. . . . . . 7
β’ (((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β β* β
((πβ(π β© βͺ π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ +β) |
38 | 34, 37 | syl 17 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ +β) |
39 | 38 | adantr 482 |
. . . . 5
β’ (((π β§ π β π« βͺ dom π) β§ (πβπ) = +β) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ +β) |
40 | | id 22 |
. . . . . . 7
β’ ((πβπ) = +β β (πβπ) = +β) |
41 | 40 | eqcomd 2743 |
. . . . . 6
β’ ((πβπ) = +β β +β = (πβπ)) |
42 | 41 | adantl 483 |
. . . . 5
β’ (((π β§ π β π« βͺ dom π) β§ (πβπ) = +β) β +β = (πβπ)) |
43 | 39, 42 | breqtrd 5136 |
. . . 4
β’ (((π β§ π β π« βͺ dom π) β§ (πβπ) = +β) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ (πβπ)) |
44 | | simpl 484 |
. . . . 5
β’ (((π β§ π β π« βͺ dom π) β§ Β¬ (πβπ) = +β) β (π β§ π β π« βͺ dom π)) |
45 | | rge0ssre 13380 |
. . . . . 6
β’
(0[,)+β) β β |
46 | | 0xr 11209 |
. . . . . . . 8
β’ 0 β
β* |
47 | 46 | a1i 11 |
. . . . . . 7
β’ (((π β§ π β π« βͺ dom π) β§ Β¬ (πβπ) = +β) β 0 β
β*) |
48 | | pnfxr 11216 |
. . . . . . . 8
β’ +β
β β* |
49 | 48 | a1i 11 |
. . . . . . 7
β’ (((π β§ π β π« βͺ dom π) β§ Β¬ (πβπ) = +β) β +β β
β*) |
50 | 44, 35 | syl 17 |
. . . . . . 7
β’ (((π β§ π β π« βͺ dom π) β§ Β¬ (πβπ) = +β) β (πβπ) β (0[,]+β)) |
51 | 40 | necon3bi 2971 |
. . . . . . . 8
β’ (Β¬
(πβπ) = +β β (πβπ) β +β) |
52 | 51 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β π« βͺ dom π) β§ Β¬ (πβπ) = +β) β (πβπ) β +β) |
53 | 47, 49, 50, 52 | eliccelicod 43842 |
. . . . . 6
β’ (((π β§ π β π« βͺ dom π) β§ Β¬ (πβπ) = +β) β (πβπ) β (0[,)+β)) |
54 | 45, 53 | sselid 3947 |
. . . . 5
β’ (((π β§ π β π« βͺ dom π) β§ Β¬ (πβπ) = +β) β (πβπ) β β) |
55 | 23 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β§ π₯ β β+) β π β
OutMeas) |
56 | 30 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β§ π₯ β β+) β π β βͺ dom π) |
57 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β (πβπ) β β) |
58 | 57 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β§ π₯ β β+) β (πβπ) β β) |
59 | | carageniuncl.3 |
. . . . . . . . 9
β’ (π β π β β€) |
60 | 59 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β§ π₯ β β+) β π β
β€) |
61 | 4 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β§ π₯ β β+) β πΈ:πβΆπ) |
62 | | simpr 486 |
. . . . . . . 8
β’ ((((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β§ π₯ β β+) β π₯ β
β+) |
63 | | eqid 2737 |
. . . . . . . 8
β’ (π β π β¦ βͺ
π β (π...π)(πΈβπ)) = (π β π β¦ βͺ
π β (π...π)(πΈβπ)) |
64 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (πΈβπ) = (πΈβπ)) |
65 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = π β (π..^π) = (π..^π)) |
66 | 65 | iuneq1d 4986 |
. . . . . . . . . 10
β’ (π = π β βͺ
π β (π..^π)(πΈβπ) = βͺ π β (π..^π)(πΈβπ)) |
67 | 64, 66 | difeq12d 4088 |
. . . . . . . . 9
β’ (π = π β ((πΈβπ) β βͺ
π β (π..^π)(πΈβπ)) = ((πΈβπ) β βͺ
π β (π..^π)(πΈβπ))) |
68 | 67 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β π β¦ ((πΈβπ) β βͺ
π β (π..^π)(πΈβπ))) = (π β π β¦ ((πΈβπ) β βͺ
π β (π..^π)(πΈβπ))) |
69 | 55, 3, 2, 56, 58, 60, 14, 61, 62, 63, 68 | carageniuncllem2 44837 |
. . . . . . 7
β’ ((((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β§ π₯ β β+) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ ((πβπ) + π₯)) |
70 | 69 | ralrimiva 3144 |
. . . . . 6
β’ (((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β βπ₯ β β+
((πβ(π β© βͺ π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ ((πβπ) + π₯)) |
71 | 34 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β
β*) |
72 | | xralrple 13131 |
. . . . . . 7
β’ ((((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β β* β§ (πβπ) β β) β (((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ (πβπ) β βπ₯ β β+ ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ ((πβπ) + π₯))) |
73 | 71, 57, 72 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β (((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ (πβπ) β βπ₯ β β+ ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ ((πβπ) + π₯))) |
74 | 70, 73 | mpbird 257 |
. . . . 5
β’ (((π β§ π β π« βͺ dom π) β§ (πβπ) β β) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ (πβπ)) |
75 | 44, 54, 74 | syl2anc 585 |
. . . 4
β’ (((π β§ π β π« βͺ dom π) β§ Β¬ (πβπ) = +β) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ (πβπ)) |
76 | 43, 75 | pm2.61dan 812 |
. . 3
β’ ((π β§ π β π« βͺ dom π) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) β€ (πβπ)) |
77 | 23, 2, 30 | omelesplit 44833 |
. . 3
β’ ((π β§ π β π« βͺ dom π) β (πβπ) β€ ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ))))) |
78 | 34, 36, 76, 77 | xrletrid 13081 |
. 2
β’ ((π β§ π β π« βͺ dom π) β ((πβ(π β© βͺ
π β π (πΈβπ))) +π (πβ(π β βͺ
π β π (πΈβπ)))) = (πβπ)) |
79 | 1, 2, 3, 21, 78 | carageneld 44817 |
1
β’ (π β βͺ π β π (πΈβπ) β π) |