Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’
(β€β₯βπ΄) = (β€β₯βπ΄) |
2 | | caubl.2 |
. . . 4
β’ (π β π· β (βMetβπ)) |
3 | 2 | 3ad2ant1 1134 |
. . 3
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β π· β (βMetβπ)) |
4 | | caublcls.6 |
. . . 4
β’ π½ = (MetOpenβπ·) |
5 | 4 | mopntopon 23945 |
. . 3
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
6 | 3, 5 | syl 17 |
. 2
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β π½ β (TopOnβπ)) |
7 | | simp3 1139 |
. . 3
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β π΄ β β) |
8 | 7 | nnzd 12585 |
. 2
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β π΄ β β€) |
9 | | simp2 1138 |
. 2
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β (1st
β πΉ)(βπ‘βπ½)π) |
10 | | 2fveq3 6897 |
. . . . . . . 8
β’ (π = π΄ β ((ballβπ·)β(πΉβπ)) = ((ballβπ·)β(πΉβπ΄))) |
11 | 10 | sseq1d 4014 |
. . . . . . 7
β’ (π = π΄ β (((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβπ΄)))) |
12 | 11 | imbi2d 341 |
. . . . . 6
β’ (π = π΄ β (((π β§ π΄ β β) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄))) β ((π β§ π΄ β β) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβπ΄))))) |
13 | | 2fveq3 6897 |
. . . . . . . 8
β’ (π = π β ((ballβπ·)β(πΉβπ)) = ((ballβπ·)β(πΉβπ))) |
14 | 13 | sseq1d 4014 |
. . . . . . 7
β’ (π = π β (((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄)))) |
15 | 14 | imbi2d 341 |
. . . . . 6
β’ (π = π β (((π β§ π΄ β β) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄))) β ((π β§ π΄ β β) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄))))) |
16 | | 2fveq3 6897 |
. . . . . . . 8
β’ (π = (π + 1) β ((ballβπ·)β(πΉβπ)) = ((ballβπ·)β(πΉβ(π + 1)))) |
17 | 16 | sseq1d 4014 |
. . . . . . 7
β’ (π = (π + 1) β (((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ΄)))) |
18 | 17 | imbi2d 341 |
. . . . . 6
β’ (π = (π + 1) β (((π β§ π΄ β β) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄))) β ((π β§ π΄ β β) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ΄))))) |
19 | | ssid 4005 |
. . . . . . 7
β’
((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβπ΄)) |
20 | 19 | 2a1i 12 |
. . . . . 6
β’ (π΄ β β€ β ((π β§ π΄ β β) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβπ΄)))) |
21 | | caubl.4 |
. . . . . . . . . . 11
β’ (π β βπ β β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ))) |
22 | | eluznn 12902 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β
(β€β₯βπ΄)) β π β β) |
23 | | fvoveq1 7432 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
24 | 23 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (π = π β ((ballβπ·)β(πΉβ(π + 1))) = ((ballβπ·)β(πΉβ(π + 1)))) |
25 | | 2fveq3 6897 |
. . . . . . . . . . . . 13
β’ (π = π β ((ballβπ·)β(πΉβπ)) = ((ballβπ·)β(πΉβπ))) |
26 | 24, 25 | sseq12d 4016 |
. . . . . . . . . . . 12
β’ (π = π β (((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ)))) |
27 | 26 | rspccva 3612 |
. . . . . . . . . . 11
β’
((βπ β
β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ)) β§ π β β) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ))) |
28 | 21, 22, 27 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ (π΄ β β β§ π β (β€β₯βπ΄))) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ))) |
29 | 28 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ))) |
30 | | sstr2 3990 |
. . . . . . . . 9
β’
(((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ)) β (((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ΄)))) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β (((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ΄)))) |
32 | 31 | expcom 415 |
. . . . . . 7
β’ (π β
(β€β₯βπ΄) β ((π β§ π΄ β β) β (((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄)) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ΄))))) |
33 | 32 | a2d 29 |
. . . . . 6
β’ (π β
(β€β₯βπ΄) β (((π β§ π΄ β β) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄))) β ((π β§ π΄ β β) β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ΄))))) |
34 | 12, 15, 18, 15, 20, 33 | uzind4 12890 |
. . . . 5
β’ (π β
(β€β₯βπ΄) β ((π β§ π΄ β β) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄)))) |
35 | 34 | impcom 409 |
. . . 4
β’ (((π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄))) |
36 | 35 | 3adantl2 1168 |
. . 3
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β ((ballβπ·)β(πΉβπ)) β ((ballβπ·)β(πΉβπ΄))) |
37 | 3 | adantr 482 |
. . . . 5
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β π· β (βMetβπ)) |
38 | | simpl1 1192 |
. . . . . . . 8
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β π) |
39 | | caubl.3 |
. . . . . . . 8
β’ (π β πΉ:ββΆ(π Γ
β+)) |
40 | 38, 39 | syl 17 |
. . . . . . 7
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β πΉ:ββΆ(π Γ
β+)) |
41 | 22 | 3ad2antl3 1188 |
. . . . . . 7
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β π β β) |
42 | 40, 41 | ffvelcdmd 7088 |
. . . . . 6
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β (πΉβπ) β (π Γ
β+)) |
43 | | xp1st 8007 |
. . . . . 6
β’ ((πΉβπ) β (π Γ β+) β
(1st β(πΉβπ)) β π) |
44 | 42, 43 | syl 17 |
. . . . 5
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β (1st
β(πΉβπ)) β π) |
45 | | xp2nd 8008 |
. . . . . 6
β’ ((πΉβπ) β (π Γ β+) β
(2nd β(πΉβπ)) β
β+) |
46 | 42, 45 | syl 17 |
. . . . 5
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β (2nd
β(πΉβπ)) β
β+) |
47 | | blcntr 23919 |
. . . . 5
β’ ((π· β (βMetβπ) β§ (1st
β(πΉβπ)) β π β§ (2nd β(πΉβπ)) β β+) β
(1st β(πΉβπ)) β ((1st β(πΉβπ))(ballβπ·)(2nd β(πΉβπ)))) |
48 | 37, 44, 46, 47 | syl3anc 1372 |
. . . 4
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β (1st
β(πΉβπ)) β ((1st
β(πΉβπ))(ballβπ·)(2nd β(πΉβπ)))) |
49 | | fvco3 6991 |
. . . . 5
β’ ((πΉ:ββΆ(π Γ β+)
β§ π β β)
β ((1st β πΉ)βπ) = (1st β(πΉβπ))) |
50 | 40, 41, 49 | syl2anc 585 |
. . . 4
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β ((1st
β πΉ)βπ) = (1st
β(πΉβπ))) |
51 | | 1st2nd2 8014 |
. . . . . . 7
β’ ((πΉβπ) β (π Γ β+) β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
52 | 42, 51 | syl 17 |
. . . . . 6
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
53 | 52 | fveq2d 6896 |
. . . . 5
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β ((ballβπ·)β(πΉβπ)) = ((ballβπ·)ββ¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©)) |
54 | | df-ov 7412 |
. . . . 5
β’
((1st β(πΉβπ))(ballβπ·)(2nd β(πΉβπ))) = ((ballβπ·)ββ¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
55 | 53, 54 | eqtr4di 2791 |
. . . 4
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β ((ballβπ·)β(πΉβπ)) = ((1st β(πΉβπ))(ballβπ·)(2nd β(πΉβπ)))) |
56 | 48, 50, 55 | 3eltr4d 2849 |
. . 3
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β ((1st
β πΉ)βπ) β ((ballβπ·)β(πΉβπ))) |
57 | 36, 56 | sseldd 3984 |
. 2
β’ (((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β§ π β (β€β₯βπ΄)) β ((1st
β πΉ)βπ) β ((ballβπ·)β(πΉβπ΄))) |
58 | 39 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π β§ π΄ β β) β (πΉβπ΄) β (π Γ
β+)) |
59 | 58 | 3adant2 1132 |
. . . . . 6
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β (πΉβπ΄) β (π Γ
β+)) |
60 | | 1st2nd2 8014 |
. . . . . 6
β’ ((πΉβπ΄) β (π Γ β+) β (πΉβπ΄) = β¨(1st β(πΉβπ΄)), (2nd β(πΉβπ΄))β©) |
61 | 59, 60 | syl 17 |
. . . . 5
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β (πΉβπ΄) = β¨(1st β(πΉβπ΄)), (2nd β(πΉβπ΄))β©) |
62 | 61 | fveq2d 6896 |
. . . 4
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β ((ballβπ·)β(πΉβπ΄)) = ((ballβπ·)ββ¨(1st β(πΉβπ΄)), (2nd β(πΉβπ΄))β©)) |
63 | | df-ov 7412 |
. . . 4
β’
((1st β(πΉβπ΄))(ballβπ·)(2nd β(πΉβπ΄))) = ((ballβπ·)ββ¨(1st β(πΉβπ΄)), (2nd β(πΉβπ΄))β©) |
64 | 62, 63 | eqtr4di 2791 |
. . 3
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β ((ballβπ·)β(πΉβπ΄)) = ((1st β(πΉβπ΄))(ballβπ·)(2nd β(πΉβπ΄)))) |
65 | | xp1st 8007 |
. . . . 5
β’ ((πΉβπ΄) β (π Γ β+) β
(1st β(πΉβπ΄)) β π) |
66 | 59, 65 | syl 17 |
. . . 4
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β (1st
β(πΉβπ΄)) β π) |
67 | | xp2nd 8008 |
. . . . . 6
β’ ((πΉβπ΄) β (π Γ β+) β
(2nd β(πΉβπ΄)) β
β+) |
68 | 59, 67 | syl 17 |
. . . . 5
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β (2nd
β(πΉβπ΄)) β
β+) |
69 | 68 | rpxrd 13017 |
. . . 4
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β (2nd
β(πΉβπ΄)) β
β*) |
70 | | blssm 23924 |
. . . 4
β’ ((π· β (βMetβπ) β§ (1st
β(πΉβπ΄)) β π β§ (2nd β(πΉβπ΄)) β β*) β
((1st β(πΉβπ΄))(ballβπ·)(2nd β(πΉβπ΄))) β π) |
71 | 3, 66, 69, 70 | syl3anc 1372 |
. . 3
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β ((1st
β(πΉβπ΄))(ballβπ·)(2nd β(πΉβπ΄))) β π) |
72 | 64, 71 | eqsstrd 4021 |
. 2
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β ((ballβπ·)β(πΉβπ΄)) β π) |
73 | 1, 6, 8, 9, 57, 72 | lmcls 22806 |
1
β’ ((π β§ (1st β
πΉ)(βπ‘βπ½)π β§ π΄ β β) β π β ((clsβπ½)β((ballβπ·)β(πΉβπ΄)))) |