Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . . 5
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
2 | 1 | metust 23937 |
. . . 4
β’ ((π β β
β§ π· β (PsMetβπ)) β ((π Γ π)filGenπΉ) β (UnifOnβπ)) |
3 | | cfilufbas 23664 |
. . . 4
β’ ((((π Γ π)filGenπΉ) β (UnifOnβπ) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β πΆ β (fBasβπ)) |
4 | 2, 3 | sylan 581 |
. . 3
β’ (((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β πΆ β (fBasβπ)) |
5 | | simpllr 775 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β π· β (PsMetβπ)) |
6 | | psmetf 23682 |
. . . . . 6
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
7 | | ffun 6675 |
. . . . . 6
β’ (π·:(π Γ π)βΆβ* β Fun
π·) |
8 | 5, 6, 7 | 3syl 18 |
. . . . 5
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β Fun π·) |
9 | 2 | ad2antrr 725 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β ((π Γ π)filGenπΉ) β (UnifOnβπ)) |
10 | | simplr 768 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β πΆ β
(CauFiluβ((π Γ π)filGenπΉ))) |
11 | 1 | metustfbas 23936 |
. . . . . . . 8
β’ ((π β β
β§ π· β (PsMetβπ)) β πΉ β (fBasβ(π Γ π))) |
12 | 11 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β πΉ β (fBasβ(π Γ π))) |
13 | | cnvimass 6037 |
. . . . . . . 8
β’ (β‘π· β (0[,)π₯)) β dom π· |
14 | | fdm 6681 |
. . . . . . . . 9
β’ (π·:(π Γ π)βΆβ* β dom
π· = (π Γ π)) |
15 | 5, 6, 14 | 3syl 18 |
. . . . . . . 8
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β dom π· = (π Γ π)) |
16 | 13, 15 | sseqtrid 4000 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β (β‘π· β (0[,)π₯)) β (π Γ π)) |
17 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β π₯ β
β+) |
18 | 17 | rphalfcld 12977 |
. . . . . . . . . 10
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β (π₯ / 2) β
β+) |
19 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β (β‘π· β (0[,)(π₯ / 2))) = (β‘π· β (0[,)(π₯ / 2)))) |
20 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π = (π₯ / 2) β (0[,)π) = (0[,)(π₯ / 2))) |
21 | 20 | imaeq2d 6017 |
. . . . . . . . . . 11
β’ (π = (π₯ / 2) β (β‘π· β (0[,)π)) = (β‘π· β (0[,)(π₯ / 2)))) |
22 | 21 | rspceeqv 3599 |
. . . . . . . . . 10
β’ (((π₯ / 2) β β+
β§ (β‘π· β (0[,)(π₯ / 2))) = (β‘π· β (0[,)(π₯ / 2)))) β βπ β β+ (β‘π· β (0[,)(π₯ / 2))) = (β‘π· β (0[,)π))) |
23 | 18, 19, 22 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β
βπ β
β+ (β‘π· β (0[,)(π₯ / 2))) = (β‘π· β (0[,)π))) |
24 | 1 | metustel 23929 |
. . . . . . . . . 10
β’ (π· β (PsMetβπ) β ((β‘π· β (0[,)(π₯ / 2))) β πΉ β βπ β β+ (β‘π· β (0[,)(π₯ / 2))) = (β‘π· β (0[,)π)))) |
25 | 24 | biimpar 479 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ βπ β β+
(β‘π· β (0[,)(π₯ / 2))) = (β‘π· β (0[,)π))) β (β‘π· β (0[,)(π₯ / 2))) β πΉ) |
26 | 5, 23, 25 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β (β‘π· β (0[,)(π₯ / 2))) β πΉ) |
27 | | 0xr 11210 |
. . . . . . . . . . 11
β’ 0 β
β* |
28 | 27 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ β β+
β 0 β β*) |
29 | | rpxr 12932 |
. . . . . . . . . 10
β’ (π₯ β β+
β π₯ β
β*) |
30 | | 0le0 12262 |
. . . . . . . . . . 11
β’ 0 β€
0 |
31 | 30 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ β β+
β 0 β€ 0) |
32 | | rpre 12931 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
β) |
33 | 32 | rehalfcld 12408 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π₯ / 2) β
β) |
34 | | rphalflt 12952 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π₯ / 2) < π₯) |
35 | 33, 32, 34 | ltled 11311 |
. . . . . . . . . 10
β’ (π₯ β β+
β (π₯ / 2) β€ π₯) |
36 | | icossico 13343 |
. . . . . . . . . 10
β’ (((0
β β* β§ π₯ β β*) β§ (0 β€ 0
β§ (π₯ / 2) β€ π₯)) β (0[,)(π₯ / 2)) β (0[,)π₯)) |
37 | 28, 29, 31, 35, 36 | syl22anc 838 |
. . . . . . . . 9
β’ (π₯ β β+
β (0[,)(π₯ / 2))
β (0[,)π₯)) |
38 | | imass2 6058 |
. . . . . . . . 9
β’
((0[,)(π₯ / 2))
β (0[,)π₯) β
(β‘π· β (0[,)(π₯ / 2))) β (β‘π· β (0[,)π₯))) |
39 | 17, 37, 38 | 3syl 18 |
. . . . . . . 8
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β (β‘π· β (0[,)(π₯ / 2))) β (β‘π· β (0[,)π₯))) |
40 | | sseq1 3973 |
. . . . . . . . 9
β’ (π€ = (β‘π· β (0[,)(π₯ / 2))) β (π€ β (β‘π· β (0[,)π₯)) β (β‘π· β (0[,)(π₯ / 2))) β (β‘π· β (0[,)π₯)))) |
41 | 40 | rspcev 3583 |
. . . . . . . 8
β’ (((β‘π· β (0[,)(π₯ / 2))) β πΉ β§ (β‘π· β (0[,)(π₯ / 2))) β (β‘π· β (0[,)π₯))) β βπ€ β πΉ π€ β (β‘π· β (0[,)π₯))) |
42 | 26, 39, 41 | syl2anc 585 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β
βπ€ β πΉ π€ β (β‘π· β (0[,)π₯))) |
43 | | elfg 23245 |
. . . . . . . 8
β’ (πΉ β (fBasβ(π Γ π)) β ((β‘π· β (0[,)π₯)) β ((π Γ π)filGenπΉ) β ((β‘π· β (0[,)π₯)) β (π Γ π) β§ βπ€ β πΉ π€ β (β‘π· β (0[,)π₯))))) |
44 | 43 | biimpar 479 |
. . . . . . 7
β’ ((πΉ β (fBasβ(π Γ π)) β§ ((β‘π· β (0[,)π₯)) β (π Γ π) β§ βπ€ β πΉ π€ β (β‘π· β (0[,)π₯)))) β (β‘π· β (0[,)π₯)) β ((π Γ π)filGenπΉ)) |
45 | 12, 16, 42, 44 | syl12anc 836 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β (β‘π· β (0[,)π₯)) β ((π Γ π)filGenπΉ)) |
46 | | cfiluexsm 23665 |
. . . . . 6
β’ ((((π Γ π)filGenπΉ) β (UnifOnβπ) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ)) β§ (β‘π· β (0[,)π₯)) β ((π Γ π)filGenπΉ)) β βπ¦ β πΆ (π¦ Γ π¦) β (β‘π· β (0[,)π₯))) |
47 | 9, 10, 45, 46 | syl3anc 1372 |
. . . . 5
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β
βπ¦ β πΆ (π¦ Γ π¦) β (β‘π· β (0[,)π₯))) |
48 | | funimass2 6588 |
. . . . . . 7
β’ ((Fun
π· β§ (π¦ Γ π¦) β (β‘π· β (0[,)π₯))) β (π· β (π¦ Γ π¦)) β (0[,)π₯)) |
49 | 48 | ex 414 |
. . . . . 6
β’ (Fun
π· β ((π¦ Γ π¦) β (β‘π· β (0[,)π₯)) β (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
50 | 49 | reximdv 3164 |
. . . . 5
β’ (Fun
π· β (βπ¦ β πΆ (π¦ Γ π¦) β (β‘π· β (0[,)π₯)) β βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
51 | 8, 47, 50 | sylc 65 |
. . . 4
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β§ π₯ β β+) β
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)) |
52 | 51 | ralrimiva 3140 |
. . 3
β’ (((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)) |
53 | 4, 52 | jca 513 |
. 2
β’ (((π β β
β§ π· β (PsMetβπ)) β§ πΆ β (CauFiluβ((π Γ π)filGenπΉ))) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
54 | | simprl 770 |
. . 3
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β πΆ β (fBasβπ)) |
55 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π₯ = π β (0[,)π₯) = (0[,)π)) |
56 | 55 | sseq2d 3980 |
. . . . . . . . 9
β’ (π₯ = π β ((π· β (π¦ Γ π¦)) β (0[,)π₯) β (π· β (π¦ Γ π¦)) β (0[,)π))) |
57 | 56 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = π β (βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯) β βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π))) |
58 | | simp-4r 783 |
. . . . . . . . 9
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
59 | 58 | simprd 497 |
. . . . . . . 8
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)) |
60 | | simplr 768 |
. . . . . . . 8
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β π β β+) |
61 | 57, 59, 60 | rspcdva 3584 |
. . . . . . 7
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π)) |
62 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π¦(π β β
β§ π· β (PsMetβπ)) |
63 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π¦ πΆ β (fBasβπ) |
64 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π¦β+ |
65 | | nfre1 3267 |
. . . . . . . . . . . . . 14
β’
β²π¦βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯) |
66 | 64, 65 | nfralw 3293 |
. . . . . . . . . . . . 13
β’
β²π¦βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯) |
67 | 63, 66 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π¦(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)) |
68 | 62, 67 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π¦((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
69 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π¦ π£ β ((π Γ π)filGenπΉ) |
70 | 68, 69 | nfan 1903 |
. . . . . . . . . 10
β’
β²π¦(((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) |
71 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦ π β
β+ |
72 | 70, 71 | nfan 1903 |
. . . . . . . . 9
β’
β²π¦((((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) |
73 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦(β‘π· β (0[,)π)) β π£ |
74 | 72, 73 | nfan 1903 |
. . . . . . . 8
β’
β²π¦(((((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) |
75 | 54 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β§ π¦ β πΆ) β πΆ β (fBasβπ)) |
76 | | fbelss 23207 |
. . . . . . . . . . . 12
β’ ((πΆ β (fBasβπ) β§ π¦ β πΆ) β π¦ β π) |
77 | 75, 76 | sylancom 589 |
. . . . . . . . . . 11
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β§ π¦ β πΆ) β π¦ β π) |
78 | | xpss12 5652 |
. . . . . . . . . . 11
β’ ((π¦ β π β§ π¦ β π) β (π¦ Γ π¦) β (π Γ π)) |
79 | 77, 77, 78 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β§ π¦ β πΆ) β (π¦ Γ π¦) β (π Γ π)) |
80 | | simp-6r 787 |
. . . . . . . . . . 11
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β§ π¦ β πΆ) β π· β (PsMetβπ)) |
81 | 80, 6, 14 | 3syl 18 |
. . . . . . . . . 10
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β§ π¦ β πΆ) β dom π· = (π Γ π)) |
82 | 79, 81 | sseqtrrd 3989 |
. . . . . . . . 9
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β§ π¦ β πΆ) β (π¦ Γ π¦) β dom π·) |
83 | 82 | ex 414 |
. . . . . . . 8
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β (π¦ β πΆ β (π¦ Γ π¦) β dom π·)) |
84 | 74, 83 | ralrimi 3239 |
. . . . . . 7
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β βπ¦ β πΆ (π¦ Γ π¦) β dom π·) |
85 | | r19.29r 3116 |
. . . . . . . 8
β’
((βπ¦ β
πΆ (π· β (π¦ Γ π¦)) β (0[,)π) β§ βπ¦ β πΆ (π¦ Γ π¦) β dom π·) β βπ¦ β πΆ ((π· β (π¦ Γ π¦)) β (0[,)π) β§ (π¦ Γ π¦) β dom π·)) |
86 | | sseqin2 4179 |
. . . . . . . . . . . . 13
β’ ((π¦ Γ π¦) β dom π· β (dom π· β© (π¦ Γ π¦)) = (π¦ Γ π¦)) |
87 | 86 | biimpi 215 |
. . . . . . . . . . . 12
β’ ((π¦ Γ π¦) β dom π· β (dom π· β© (π¦ Γ π¦)) = (π¦ Γ π¦)) |
88 | 87 | adantl 483 |
. . . . . . . . . . 11
β’ (((π· β (π¦ Γ π¦)) β (0[,)π) β§ (π¦ Γ π¦) β dom π·) β (dom π· β© (π¦ Γ π¦)) = (π¦ Γ π¦)) |
89 | | dminss 6109 |
. . . . . . . . . . 11
β’ (dom
π· β© (π¦ Γ π¦)) β (β‘π· β (π· β (π¦ Γ π¦))) |
90 | 88, 89 | eqsstrrdi 4003 |
. . . . . . . . . 10
β’ (((π· β (π¦ Γ π¦)) β (0[,)π) β§ (π¦ Γ π¦) β dom π·) β (π¦ Γ π¦) β (β‘π· β (π· β (π¦ Γ π¦)))) |
91 | | imass2 6058 |
. . . . . . . . . . 11
β’ ((π· β (π¦ Γ π¦)) β (0[,)π) β (β‘π· β (π· β (π¦ Γ π¦))) β (β‘π· β (0[,)π))) |
92 | 91 | adantr 482 |
. . . . . . . . . 10
β’ (((π· β (π¦ Γ π¦)) β (0[,)π) β§ (π¦ Γ π¦) β dom π·) β (β‘π· β (π· β (π¦ Γ π¦))) β (β‘π· β (0[,)π))) |
93 | 90, 92 | sstrd 3958 |
. . . . . . . . 9
β’ (((π· β (π¦ Γ π¦)) β (0[,)π) β§ (π¦ Γ π¦) β dom π·) β (π¦ Γ π¦) β (β‘π· β (0[,)π))) |
94 | 93 | reximi 3084 |
. . . . . . . 8
β’
(βπ¦ β
πΆ ((π· β (π¦ Γ π¦)) β (0[,)π) β§ (π¦ Γ π¦) β dom π·) β βπ¦ β πΆ (π¦ Γ π¦) β (β‘π· β (0[,)π))) |
95 | 85, 94 | syl 17 |
. . . . . . 7
β’
((βπ¦ β
πΆ (π· β (π¦ Γ π¦)) β (0[,)π) β§ βπ¦ β πΆ (π¦ Γ π¦) β dom π·) β βπ¦ β πΆ (π¦ Γ π¦) β (β‘π· β (0[,)π))) |
96 | 61, 84, 95 | syl2anc 585 |
. . . . . 6
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β βπ¦ β πΆ (π¦ Γ π¦) β (β‘π· β (0[,)π))) |
97 | | r19.41v 3182 |
. . . . . . 7
β’
(βπ¦ β
πΆ ((π¦ Γ π¦) β (β‘π· β (0[,)π)) β§ (β‘π· β (0[,)π)) β π£) β (βπ¦ β πΆ (π¦ Γ π¦) β (β‘π· β (0[,)π)) β§ (β‘π· β (0[,)π)) β π£)) |
98 | | sstr 3956 |
. . . . . . . 8
β’ (((π¦ Γ π¦) β (β‘π· β (0[,)π)) β§ (β‘π· β (0[,)π)) β π£) β (π¦ Γ π¦) β π£) |
99 | 98 | reximi 3084 |
. . . . . . 7
β’
(βπ¦ β
πΆ ((π¦ Γ π¦) β (β‘π· β (0[,)π)) β§ (β‘π· β (0[,)π)) β π£) β βπ¦ β πΆ (π¦ Γ π¦) β π£) |
100 | 97, 99 | sylbir 234 |
. . . . . 6
β’
((βπ¦ β
πΆ (π¦ Γ π¦) β (β‘π· β (0[,)π)) β§ (β‘π· β (0[,)π)) β π£) β βπ¦ β πΆ (π¦ Γ π¦) β π£) |
101 | 96, 100 | sylancom 589 |
. . . . 5
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π β β+) β§ (β‘π· β (0[,)π)) β π£) β βπ¦ β πΆ (π¦ Γ π¦) β π£) |
102 | | simp-5r 785 |
. . . . . . . 8
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β πΉ) β§ π€ β π£) β π· β (PsMetβπ)) |
103 | | simplr 768 |
. . . . . . . 8
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β πΉ) β§ π€ β π£) β π€ β πΉ) |
104 | 1 | metustel 23929 |
. . . . . . . . 9
β’ (π· β (PsMetβπ) β (π€ β πΉ β βπ β β+ π€ = (β‘π· β (0[,)π)))) |
105 | 104 | biimpa 478 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π€ β πΉ) β βπ β β+ π€ = (β‘π· β (0[,)π))) |
106 | 102, 103,
105 | syl2anc 585 |
. . . . . . 7
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β πΉ) β§ π€ β π£) β βπ β β+ π€ = (β‘π· β (0[,)π))) |
107 | | r19.41v 3182 |
. . . . . . . 8
β’
(βπ β
β+ (π€ =
(β‘π· β (0[,)π)) β§ π€ β π£) β (βπ β β+ π€ = (β‘π· β (0[,)π)) β§ π€ β π£)) |
108 | | sseq1 3973 |
. . . . . . . . . 10
β’ (π€ = (β‘π· β (0[,)π)) β (π€ β π£ β (β‘π· β (0[,)π)) β π£)) |
109 | 108 | biimpa 478 |
. . . . . . . . 9
β’ ((π€ = (β‘π· β (0[,)π)) β§ π€ β π£) β (β‘π· β (0[,)π)) β π£) |
110 | 109 | reximi 3084 |
. . . . . . . 8
β’
(βπ β
β+ (π€ =
(β‘π· β (0[,)π)) β§ π€ β π£) β βπ β β+ (β‘π· β (0[,)π)) β π£) |
111 | 107, 110 | sylbir 234 |
. . . . . . 7
β’
((βπ β
β+ π€ =
(β‘π· β (0[,)π)) β§ π€ β π£) β βπ β β+ (β‘π· β (0[,)π)) β π£) |
112 | 106, 111 | sylancom 589 |
. . . . . 6
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
(πΆ β (fBasβπ) β§ βπ₯ β β+
βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β πΉ) β§ π€ β π£) β βπ β β+ (β‘π· β (0[,)π)) β π£) |
113 | 11 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β πΉ β (fBasβ(π Γ π))) |
114 | | elfg 23245 |
. . . . . . . . 9
β’ (πΉ β (fBasβ(π Γ π)) β (π£ β ((π Γ π)filGenπΉ) β (π£ β (π Γ π) β§ βπ€ β πΉ π€ β π£))) |
115 | 114 | biimpa 478 |
. . . . . . . 8
β’ ((πΉ β (fBasβ(π Γ π)) β§ π£ β ((π Γ π)filGenπΉ)) β (π£ β (π Γ π) β§ βπ€ β πΉ π€ β π£)) |
116 | 113, 115 | sylancom 589 |
. . . . . . 7
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β (π£ β (π Γ π) β§ βπ€ β πΉ π€ β π£)) |
117 | 116 | simprd 497 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β βπ€ β πΉ π€ β π£) |
118 | 112, 117 | r19.29a 3156 |
. . . . 5
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β βπ β β+ (β‘π· β (0[,)π)) β π£) |
119 | 101, 118 | r19.29a 3156 |
. . . 4
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β§ π£ β ((π Γ π)filGenπΉ)) β βπ¦ β πΆ (π¦ Γ π¦) β π£) |
120 | 119 | ralrimiva 3140 |
. . 3
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β βπ£ β ((π Γ π)filGenπΉ)βπ¦ β πΆ (π¦ Γ π¦) β π£) |
121 | 2 | adantr 482 |
. . . 4
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β ((π Γ π)filGenπΉ) β (UnifOnβπ)) |
122 | | iscfilu 23663 |
. . . 4
β’ (((π Γ π)filGenπΉ) β (UnifOnβπ) β (πΆ β (CauFiluβ((π Γ π)filGenπΉ)) β (πΆ β (fBasβπ) β§ βπ£ β ((π Γ π)filGenπΉ)βπ¦ β πΆ (π¦ Γ π¦) β π£))) |
123 | 121, 122 | syl 17 |
. . 3
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β (πΆ β (CauFiluβ((π Γ π)filGenπΉ)) β (πΆ β (fBasβπ) β§ βπ£ β ((π Γ π)filGenπΉ)βπ¦ β πΆ (π¦ Γ π¦) β π£))) |
124 | 54, 120, 123 | mpbir2and 712 |
. 2
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯))) β πΆ β (CauFiluβ((π Γ π)filGenπΉ))) |
125 | 53, 124 | impbida 800 |
1
β’ ((π β β
β§ π· β (PsMetβπ)) β (πΆ β (CauFiluβ((π Γ π)filGenπΉ)) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) |