Step | Hyp | Ref
| Expression |
1 | | itgulm.z |
. . . 4
β’ π =
(β€β₯βπ) |
2 | | itgulm.m |
. . . 4
β’ (π β π β β€) |
3 | | itgulm.f |
. . . . . 6
β’ (π β πΉ:πβΆπΏ1) |
4 | 3 | ffnd 6674 |
. . . . 5
β’ (π β πΉ Fn π) |
5 | | itgulm.u |
. . . . 5
β’ (π β πΉ(βπ’βπ)πΊ) |
6 | | ulmf2 25759 |
. . . . 5
β’ ((πΉ Fn π β§ πΉ(βπ’βπ)πΊ) β πΉ:πβΆ(β βm π)) |
7 | 4, 5, 6 | syl2anc 585 |
. . . 4
β’ (π β πΉ:πβΆ(β βm π)) |
8 | | eqidd 2738 |
. . . 4
β’ ((π β§ (π β π β§ π₯ β π)) β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
9 | | eqidd 2738 |
. . . 4
β’ ((π β§ π₯ β π) β (πΊβπ₯) = (πΊβπ₯)) |
10 | | 1rp 12926 |
. . . . 5
β’ 1 β
β+ |
11 | 10 | a1i 11 |
. . . 4
β’ (π β 1 β
β+) |
12 | 1, 2, 7, 8, 9, 5, 11 | ulmi 25761 |
. . 3
β’ (π β βπ β π βπ β (β€β₯βπ)βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1) |
13 | 1 | r19.2uz 15243 |
. . 3
β’
(βπ β
π βπ β
(β€β₯βπ)βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1 β βπ β π βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1) |
14 | 12, 13 | syl 17 |
. 2
β’ (π β βπ β π βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1) |
15 | | ulmcl 25756 |
. . . . . . 7
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) |
16 | 5, 15 | syl 17 |
. . . . . 6
β’ (π β πΊ:πβΆβ) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β πΊ:πβΆβ) |
18 | 17 | feqmptd 6915 |
. . . 4
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β πΊ = (π§ β π β¦ (πΊβπ§))) |
19 | 7 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ) β (β βm π)) |
20 | | elmapi 8794 |
. . . . . . . . 9
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ):πβΆβ) |
22 | 21 | adantrr 716 |
. . . . . . 7
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (πΉβπ):πβΆβ) |
23 | 22 | ffvelcdmda 7040 |
. . . . . 6
β’ (((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β§ π§ β π) β ((πΉβπ)βπ§) β β) |
24 | 17 | ffvelcdmda 7040 |
. . . . . 6
β’ (((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β§ π§ β π) β (πΊβπ§) β β) |
25 | 23, 24 | nncand 11524 |
. . . . 5
β’ (((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β§ π§ β π) β (((πΉβπ)βπ§) β (((πΉβπ)βπ§) β (πΊβπ§))) = (πΊβπ§)) |
26 | 25 | mpteq2dva 5210 |
. . . 4
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (π§ β π β¦ (((πΉβπ)βπ§) β (((πΉβπ)βπ§) β (πΊβπ§)))) = (π§ β π β¦ (πΊβπ§))) |
27 | 18, 26 | eqtr4d 2780 |
. . 3
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β πΊ = (π§ β π β¦ (((πΉβπ)βπ§) β (((πΉβπ)βπ§) β (πΊβπ§))))) |
28 | 22 | feqmptd 6915 |
. . . . 5
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (πΉβπ) = (π§ β π β¦ ((πΉβπ)βπ§))) |
29 | 3 | ffvelcdmda 7040 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β
πΏ1) |
30 | 29 | adantrr 716 |
. . . . 5
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (πΉβπ) β
πΏ1) |
31 | 28, 30 | eqeltrrd 2839 |
. . . 4
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (π§ β π β¦ ((πΉβπ)βπ§)) β
πΏ1) |
32 | 23, 24 | subcld 11519 |
. . . 4
β’ (((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β§ π§ β π) β (((πΉβπ)βπ§) β (πΊβπ§)) β β) |
33 | | ulmscl 25754 |
. . . . . . . . 9
β’ (πΉ(βπ’βπ)πΊ β π β V) |
34 | 5, 33 | syl 17 |
. . . . . . . 8
β’ (π β π β V) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β π β V) |
36 | 35, 23, 24, 28, 18 | offval2 7642 |
. . . . . 6
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β ((πΉβπ) βf β πΊ) = (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))) |
37 | | iblmbf 25148 |
. . . . . . . 8
β’ ((πΉβπ) β πΏ1 β (πΉβπ) β MblFn) |
38 | 30, 37 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (πΉβπ) β MblFn) |
39 | | iblmbf 25148 |
. . . . . . . . . . 11
β’ (π₯ β πΏ1
β π₯ β
MblFn) |
40 | 39 | ssriv 3953 |
. . . . . . . . . 10
β’
πΏ1 β MblFn |
41 | | fss 6690 |
. . . . . . . . . 10
β’ ((πΉ:πβΆπΏ1 β§
πΏ1 β MblFn) β πΉ:πβΆMblFn) |
42 | 3, 40, 41 | sylancl 587 |
. . . . . . . . 9
β’ (π β πΉ:πβΆMblFn) |
43 | 1, 2, 42, 5 | mbfulm 25781 |
. . . . . . . 8
β’ (π β πΊ β MblFn) |
44 | 43 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β πΊ β MblFn) |
45 | 38, 44 | mbfsub 25042 |
. . . . . 6
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β ((πΉβπ) βf β πΊ) β MblFn) |
46 | 36, 45 | eqeltrrd 2839 |
. . . . 5
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§))) β MblFn) |
47 | | eqid 2737 |
. . . . . . . 8
β’ (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§))) = (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§))) |
48 | 47, 32 | dmmptd 6651 |
. . . . . . 7
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β dom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§))) = π) |
49 | 48 | fveq2d 6851 |
. . . . . 6
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (volβdom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))) = (volβπ)) |
50 | | itgulm.s |
. . . . . . 7
β’ (π β (volβπ) β
β) |
51 | 50 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (volβπ) β
β) |
52 | 49, 51 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (volβdom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))) β β) |
53 | | 1re 11162 |
. . . . . 6
β’ 1 β
β |
54 | 21 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π₯ β π) β ((πΉβπ)βπ₯) β β) |
55 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β πΊ:πβΆβ) |
56 | 55 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π₯ β π) β (πΊβπ₯) β β) |
57 | 54, 56 | subcld 11519 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π₯ β π) β (((πΉβπ)βπ₯) β (πΊβπ₯)) β β) |
58 | 57 | abscld 15328 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π₯ β π) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β β) |
59 | | ltle 11250 |
. . . . . . . . . . 11
β’
(((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β β β§ 1 β β)
β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1 β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β€ 1)) |
60 | 58, 53, 59 | sylancl 587 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π₯ β π) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1 β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β€ 1)) |
61 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π§ = π₯ β ((πΉβπ)βπ§) = ((πΉβπ)βπ₯)) |
62 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π§ = π₯ β (πΊβπ§) = (πΊβπ₯)) |
63 | 61, 62 | oveq12d 7380 |
. . . . . . . . . . . . . 14
β’ (π§ = π₯ β (((πΉβπ)βπ§) β (πΊβπ§)) = (((πΉβπ)βπ₯) β (πΊβπ₯))) |
64 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ)βπ₯) β (πΊβπ₯)) β V |
65 | 63, 47, 64 | fvmpt 6953 |
. . . . . . . . . . . . 13
β’ (π₯ β π β ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯) = (((πΉβπ)βπ₯) β (πΊβπ₯))) |
66 | 65 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π₯ β π) β ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯) = (((πΉβπ)βπ₯) β (πΊβπ₯))) |
67 | 66 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π₯ β π) β (absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) = (absβ(((πΉβπ)βπ₯) β (πΊβπ₯)))) |
68 | 67 | breq1d 5120 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π₯ β π) β ((absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ 1 β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β€ 1)) |
69 | 60, 68 | sylibrd 259 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π₯ β π) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1 β (absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ 1)) |
70 | 69 | ralimdva 3165 |
. . . . . . . 8
β’ ((π β§ π β π) β (βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1 β βπ₯ β π (absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ 1)) |
71 | 70 | impr 456 |
. . . . . . 7
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β βπ₯ β π (absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ 1) |
72 | 48 | raleqdv 3316 |
. . . . . . 7
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (βπ₯ β dom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))(absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ 1 β βπ₯ β π (absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ 1)) |
73 | 71, 72 | mpbird 257 |
. . . . . 6
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β βπ₯ β dom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))(absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ 1) |
74 | | brralrspcev 5170 |
. . . . . 6
β’ ((1
β β β§ βπ₯ β dom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))(absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ 1) β βπ β β βπ₯ β dom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))(absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ π) |
75 | 53, 73, 74 | sylancr 588 |
. . . . 5
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β βπ β β βπ₯ β dom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))(absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ π) |
76 | | bddibl 25220 |
. . . . 5
β’ (((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§))) β MblFn β§ (volβdom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))) β β β§ βπ β β βπ₯ β dom (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))(absβ((π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§)))βπ₯)) β€ π) β (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§))) β
πΏ1) |
77 | 46, 52, 75, 76 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (π§ β π β¦ (((πΉβπ)βπ§) β (πΊβπ§))) β
πΏ1) |
78 | 23, 31, 32, 77 | iblsub 25202 |
. . 3
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β (π§ β π β¦ (((πΉβπ)βπ§) β (((πΉβπ)βπ§) β (πΊβπ§)))) β
πΏ1) |
79 | 27, 78 | eqeltrd 2838 |
. 2
β’ ((π β§ (π β π β§ βπ₯ β π (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < 1)) β πΊ β
πΏ1) |
80 | 14, 79 | rexlimddv 3159 |
1
β’ (π β πΊ β
πΏ1) |