Step | Hyp | Ref
| Expression |
1 | | phtpycc.3 |
. 2
β’ (π β πΉ β (II Cn π½)) |
2 | | phtpycc.5 |
. 2
β’ (π β π» β (II Cn π½)) |
3 | | phtpycc.1 |
. . 3
β’ π = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ if(π¦ β€ (1 / 2), (π₯πΎ(2 Β· π¦)), (π₯πΏ((2 Β· π¦) β 1)))) |
4 | | iitopon 24386 |
. . . 4
β’ II β
(TopOnβ(0[,]1)) |
5 | 4 | a1i 11 |
. . 3
β’ (π β II β
(TopOnβ(0[,]1))) |
6 | | phtpycc.4 |
. . 3
β’ (π β πΊ β (II Cn π½)) |
7 | 1, 6 | phtpyhtpy 24489 |
. . . 4
β’ (π β (πΉ(PHtpyβπ½)πΊ) β (πΉ(II Htpy π½)πΊ)) |
8 | | phtpycc.6 |
. . . 4
β’ (π β πΎ β (πΉ(PHtpyβπ½)πΊ)) |
9 | 7, 8 | sseldd 3982 |
. . 3
β’ (π β πΎ β (πΉ(II Htpy π½)πΊ)) |
10 | 6, 2 | phtpyhtpy 24489 |
. . . 4
β’ (π β (πΊ(PHtpyβπ½)π») β (πΊ(II Htpy π½)π»)) |
11 | | phtpycc.7 |
. . . 4
β’ (π β πΏ β (πΊ(PHtpyβπ½)π»)) |
12 | 10, 11 | sseldd 3982 |
. . 3
β’ (π β πΏ β (πΊ(II Htpy π½)π»)) |
13 | 3, 5, 1, 6, 2, 9, 12 | htpycc 24487 |
. 2
β’ (π β π β (πΉ(II Htpy π½)π»)) |
14 | | 0elunit 13442 |
. . . 4
β’ 0 β
(0[,]1) |
15 | | simpr 485 |
. . . 4
β’ ((π β§ π β (0[,]1)) β π β (0[,]1)) |
16 | | simpr 485 |
. . . . . . 7
β’ ((π₯ = 0 β§ π¦ = π ) β π¦ = π ) |
17 | 16 | breq1d 5157 |
. . . . . 6
β’ ((π₯ = 0 β§ π¦ = π ) β (π¦ β€ (1 / 2) β π β€ (1 / 2))) |
18 | | simpl 483 |
. . . . . . 7
β’ ((π₯ = 0 β§ π¦ = π ) β π₯ = 0) |
19 | 16 | oveq2d 7421 |
. . . . . . 7
β’ ((π₯ = 0 β§ π¦ = π ) β (2 Β· π¦) = (2 Β· π )) |
20 | 18, 19 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = 0 β§ π¦ = π ) β (π₯πΎ(2 Β· π¦)) = (0πΎ(2 Β· π ))) |
21 | 19 | oveq1d 7420 |
. . . . . . 7
β’ ((π₯ = 0 β§ π¦ = π ) β ((2 Β· π¦) β 1) = ((2 Β· π ) β 1)) |
22 | 18, 21 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = 0 β§ π¦ = π ) β (π₯πΏ((2 Β· π¦) β 1)) = (0πΏ((2 Β· π ) β 1))) |
23 | 17, 20, 22 | ifbieq12d 4555 |
. . . . 5
β’ ((π₯ = 0 β§ π¦ = π ) β if(π¦ β€ (1 / 2), (π₯πΎ(2 Β· π¦)), (π₯πΏ((2 Β· π¦) β 1))) = if(π β€ (1 / 2), (0πΎ(2 Β· π )), (0πΏ((2 Β· π ) β 1)))) |
24 | | ovex 7438 |
. . . . . 6
β’ (0πΎ(2 Β· π )) β V |
25 | | ovex 7438 |
. . . . . 6
β’ (0πΏ((2 Β· π ) β 1)) β V |
26 | 24, 25 | ifex 4577 |
. . . . 5
β’ if(π β€ (1 / 2), (0πΎ(2 Β· π )), (0πΏ((2 Β· π ) β 1))) β V |
27 | 23, 3, 26 | ovmpoa 7559 |
. . . 4
β’ ((0
β (0[,]1) β§ π
β (0[,]1)) β (0ππ ) = if(π β€ (1 / 2), (0πΎ(2 Β· π )), (0πΏ((2 Β· π ) β 1)))) |
28 | 14, 15, 27 | sylancr 587 |
. . 3
β’ ((π β§ π β (0[,]1)) β (0ππ ) = if(π β€ (1 / 2), (0πΎ(2 Β· π )), (0πΏ((2 Β· π ) β 1)))) |
29 | | simpll 765 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β π) |
30 | | elii1 24442 |
. . . . . . . 8
β’ (π β (0[,](1 / 2)) β
(π β (0[,]1) β§
π β€ (1 /
2))) |
31 | | iihalf1 24438 |
. . . . . . . 8
β’ (π β (0[,](1 / 2)) β (2
Β· π ) β
(0[,]1)) |
32 | 30, 31 | sylbir 234 |
. . . . . . 7
β’ ((π β (0[,]1) β§ π β€ (1 / 2)) β (2
Β· π ) β
(0[,]1)) |
33 | 32 | adantll 712 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β (2 Β· π ) β
(0[,]1)) |
34 | 1, 6, 8 | phtpyi 24491 |
. . . . . 6
β’ ((π β§ (2 Β· π ) β (0[,]1)) β
((0πΎ(2 Β· π )) = (πΉβ0) β§ (1πΎ(2 Β· π )) = (πΉβ1))) |
35 | 29, 33, 34 | syl2anc 584 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β ((0πΎ(2 Β· π )) = (πΉβ0) β§ (1πΎ(2 Β· π )) = (πΉβ1))) |
36 | 35 | simpld 495 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β (0πΎ(2 Β· π )) = (πΉβ0)) |
37 | | simpll 765 |
. . . . . . 7
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β π) |
38 | | elii2 24443 |
. . . . . . . . 9
β’ ((π β (0[,]1) β§ Β¬
π β€ (1 / 2)) β
π β ((1 /
2)[,]1)) |
39 | | iihalf2 24440 |
. . . . . . . . 9
β’ (π β ((1 / 2)[,]1) β ((2
Β· π ) β 1)
β (0[,]1)) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
β’ ((π β (0[,]1) β§ Β¬
π β€ (1 / 2)) β ((2
Β· π ) β 1)
β (0[,]1)) |
41 | 40 | adantll 712 |
. . . . . . 7
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β ((2
Β· π ) β 1)
β (0[,]1)) |
42 | 6, 2, 11 | phtpyi 24491 |
. . . . . . 7
β’ ((π β§ ((2 Β· π ) β 1) β (0[,]1))
β ((0πΏ((2 Β·
π ) β 1)) = (πΊβ0) β§ (1πΏ((2 Β· π ) β 1)) = (πΊβ1))) |
43 | 37, 41, 42 | syl2anc 584 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β ((0πΏ((2 Β· π ) β 1)) = (πΊβ0) β§ (1πΏ((2 Β· π ) β 1)) = (πΊβ1))) |
44 | 43 | simpld 495 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β (0πΏ((2 Β· π ) β 1)) = (πΊβ0)) |
45 | 1, 6, 8 | phtpy01 24492 |
. . . . . . 7
β’ (π β ((πΉβ0) = (πΊβ0) β§ (πΉβ1) = (πΊβ1))) |
46 | 45 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β ((πΉβ0) = (πΊβ0) β§ (πΉβ1) = (πΊβ1))) |
47 | 46 | simpld 495 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β (πΉβ0) = (πΊβ0)) |
48 | 44, 47 | eqtr4d 2775 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β (0πΏ((2 Β· π ) β 1)) = (πΉβ0)) |
49 | 36, 48 | ifeqda 4563 |
. . 3
β’ ((π β§ π β (0[,]1)) β if(π β€ (1 / 2), (0πΎ(2 Β· π )), (0πΏ((2 Β· π ) β 1))) = (πΉβ0)) |
50 | 28, 49 | eqtrd 2772 |
. 2
β’ ((π β§ π β (0[,]1)) β (0ππ ) = (πΉβ0)) |
51 | | 1elunit 13443 |
. . . 4
β’ 1 β
(0[,]1) |
52 | | simpr 485 |
. . . . . . 7
β’ ((π₯ = 1 β§ π¦ = π ) β π¦ = π ) |
53 | 52 | breq1d 5157 |
. . . . . 6
β’ ((π₯ = 1 β§ π¦ = π ) β (π¦ β€ (1 / 2) β π β€ (1 / 2))) |
54 | | simpl 483 |
. . . . . . 7
β’ ((π₯ = 1 β§ π¦ = π ) β π₯ = 1) |
55 | 52 | oveq2d 7421 |
. . . . . . 7
β’ ((π₯ = 1 β§ π¦ = π ) β (2 Β· π¦) = (2 Β· π )) |
56 | 54, 55 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = 1 β§ π¦ = π ) β (π₯πΎ(2 Β· π¦)) = (1πΎ(2 Β· π ))) |
57 | 55 | oveq1d 7420 |
. . . . . . 7
β’ ((π₯ = 1 β§ π¦ = π ) β ((2 Β· π¦) β 1) = ((2 Β· π ) β 1)) |
58 | 54, 57 | oveq12d 7423 |
. . . . . 6
β’ ((π₯ = 1 β§ π¦ = π ) β (π₯πΏ((2 Β· π¦) β 1)) = (1πΏ((2 Β· π ) β 1))) |
59 | 53, 56, 58 | ifbieq12d 4555 |
. . . . 5
β’ ((π₯ = 1 β§ π¦ = π ) β if(π¦ β€ (1 / 2), (π₯πΎ(2 Β· π¦)), (π₯πΏ((2 Β· π¦) β 1))) = if(π β€ (1 / 2), (1πΎ(2 Β· π )), (1πΏ((2 Β· π ) β 1)))) |
60 | | ovex 7438 |
. . . . . 6
β’ (1πΎ(2 Β· π )) β V |
61 | | ovex 7438 |
. . . . . 6
β’ (1πΏ((2 Β· π ) β 1)) β V |
62 | 60, 61 | ifex 4577 |
. . . . 5
β’ if(π β€ (1 / 2), (1πΎ(2 Β· π )), (1πΏ((2 Β· π ) β 1))) β V |
63 | 59, 3, 62 | ovmpoa 7559 |
. . . 4
β’ ((1
β (0[,]1) β§ π
β (0[,]1)) β (1ππ ) = if(π β€ (1 / 2), (1πΎ(2 Β· π )), (1πΏ((2 Β· π ) β 1)))) |
64 | 51, 15, 63 | sylancr 587 |
. . 3
β’ ((π β§ π β (0[,]1)) β (1ππ ) = if(π β€ (1 / 2), (1πΎ(2 Β· π )), (1πΏ((2 Β· π ) β 1)))) |
65 | 35 | simprd 496 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ π β€ (1 / 2)) β (1πΎ(2 Β· π )) = (πΉβ1)) |
66 | 43 | simprd 496 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β (1πΏ((2 Β· π ) β 1)) = (πΊβ1)) |
67 | 46 | simprd 496 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β (πΉβ1) = (πΊβ1)) |
68 | 66, 67 | eqtr4d 2775 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ Β¬ π β€ (1 / 2)) β (1πΏ((2 Β· π ) β 1)) = (πΉβ1)) |
69 | 65, 68 | ifeqda 4563 |
. . 3
β’ ((π β§ π β (0[,]1)) β if(π β€ (1 / 2), (1πΎ(2 Β· π )), (1πΏ((2 Β· π ) β 1))) = (πΉβ1)) |
70 | 64, 69 | eqtrd 2772 |
. 2
β’ ((π β§ π β (0[,]1)) β (1ππ ) = (πΉβ1)) |
71 | 1, 2, 13, 50, 70 | isphtpyd 24493 |
1
β’ (π β π β (πΉ(PHtpyβπ½)π»)) |