Step | Hyp | Ref
| Expression |
1 | | df-ioo 13126 |
. . . . . . . . . 10
β’ (,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) |
2 | 1 | ixxf 13132 |
. . . . . . . . 9
β’
(,):(β* Γ β*)βΆπ«
β* |
3 | | ffn 6627 |
. . . . . . . . 9
β’
((,):(β* Γ β*)βΆπ«
β* β (,) Fn (β* Γ
β*)) |
4 | 2, 3 | mp1i 13 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β (,) Fn
(β* Γ β*)) |
5 | | elssuni 4878 |
. . . . . . . . . . . . . 14
β’ (π΄ β (π½ Γt π½) β π΄ β βͺ (π½ Γt π½)) |
6 | | tpr2rico.0 |
. . . . . . . . . . . . . . . 16
β’ π½ = (topGenβran
(,)) |
7 | | retop 23967 |
. . . . . . . . . . . . . . . 16
β’
(topGenβran (,)) β Top |
8 | 6, 7 | eqeltri 2833 |
. . . . . . . . . . . . . . 15
β’ π½ β Top |
9 | | uniretop 23968 |
. . . . . . . . . . . . . . . 16
β’ β =
βͺ (topGenβran (,)) |
10 | 6 | unieqi 4858 |
. . . . . . . . . . . . . . . 16
β’ βͺ π½ =
βͺ (topGenβran (,)) |
11 | 9, 10 | eqtr4i 2767 |
. . . . . . . . . . . . . . 15
β’ β =
βͺ π½ |
12 | 8, 8, 11, 11 | txunii 22786 |
. . . . . . . . . . . . . 14
β’ (β
Γ β) = βͺ (π½ Γt π½) |
13 | 5, 12 | sseqtrrdi 3978 |
. . . . . . . . . . . . 13
β’ (π΄ β (π½ Γt π½) β π΄ β (β Γ
β)) |
14 | 13 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β π΄ β (β Γ
β)) |
15 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β π β π΄) |
16 | 14, 15 | sseldd 3928 |
. . . . . . . . . . 11
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β π β (β Γ
β)) |
17 | | xp1st 7892 |
. . . . . . . . . . 11
β’ (π β (β Γ
β) β (1st βπ) β β) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(1st βπ)
β β) |
19 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β π β
β+) |
20 | 19 | rpred 12815 |
. . . . . . . . . . 11
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β π β
β) |
21 | 20 | rehalfcld 12263 |
. . . . . . . . . 10
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β (π / 2) β
β) |
22 | 18, 21 | resubcld 11446 |
. . . . . . . . 9
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((1st βπ)
β (π / 2)) β
β) |
23 | 22 | rexrd 11068 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((1st βπ)
β (π / 2)) β
β*) |
24 | 18, 21 | readdcld 11047 |
. . . . . . . . 9
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((1st βπ)
+ (π / 2)) β
β) |
25 | 24 | rexrd 11068 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((1st βπ)
+ (π / 2)) β
β*) |
26 | | fnovrn 7476 |
. . . . . . . 8
β’ (((,) Fn
(β* Γ β*) β§ ((1st
βπ) β (π / 2)) β
β* β§ ((1st βπ) + (π / 2)) β β*) β
(((1st βπ)
β (π /
2))(,)((1st βπ) + (π / 2))) β ran (,)) |
27 | 4, 23, 25, 26 | syl3anc 1371 |
. . . . . . 7
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(((1st βπ)
β (π /
2))(,)((1st βπ) + (π / 2))) β ran (,)) |
28 | | xp2nd 7893 |
. . . . . . . . . . 11
β’ (π β (β Γ
β) β (2nd βπ) β β) |
29 | 16, 28 | syl 17 |
. . . . . . . . . 10
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(2nd βπ)
β β) |
30 | 29, 21 | resubcld 11446 |
. . . . . . . . 9
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((2nd βπ)
β (π / 2)) β
β) |
31 | 30 | rexrd 11068 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((2nd βπ)
β (π / 2)) β
β*) |
32 | 29, 21 | readdcld 11047 |
. . . . . . . . 9
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((2nd βπ)
+ (π / 2)) β
β) |
33 | 32 | rexrd 11068 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((2nd βπ)
+ (π / 2)) β
β*) |
34 | | fnovrn 7476 |
. . . . . . . 8
β’ (((,) Fn
(β* Γ β*) β§ ((2nd
βπ) β (π / 2)) β
β* β§ ((2nd βπ) + (π / 2)) β β*) β
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))) β ran (,)) |
35 | 4, 31, 33, 34 | syl3anc 1371 |
. . . . . . 7
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))) β ran (,)) |
36 | | eqidd 2737 |
. . . . . . 7
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) = ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))))) |
37 | | xpeq1 5611 |
. . . . . . . . 9
β’ (π₯ = (((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) β (π₯ Γ π¦) = ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ π¦)) |
38 | 37 | eqeq2d 2747 |
. . . . . . . 8
β’ (π₯ = (((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) β
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) = (π₯ Γ π¦) β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) = ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ π¦))) |
39 | | xpeq2 5618 |
. . . . . . . . 9
β’ (π¦ = (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2))) β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ π¦) = ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2))))) |
40 | 39 | eqeq2d 2747 |
. . . . . . . 8
β’ (π¦ = (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2))) β
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) = ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ π¦) β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) = ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))))) |
41 | 38, 40 | rspc2ev 3578 |
. . . . . . 7
β’
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) β ran (,) β§
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))) β ran (,) β§
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) = ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))))) β βπ₯ β ran (,)βπ¦ β ran (,)((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) = (π₯ Γ π¦)) |
42 | 27, 35, 36, 41 | syl3anc 1371 |
. . . . . 6
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
βπ₯ β ran
(,)βπ¦ β ran
(,)((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) = (π₯ Γ π¦)) |
43 | | eqid 2736 |
. . . . . . 7
β’ (π₯ β ran (,), π¦ β ran (,) β¦ (π₯ Γ π¦)) = (π₯ β ran (,), π¦ β ran (,) β¦ (π₯ Γ π¦)) |
44 | | vex 3442 |
. . . . . . . 8
β’ π₯ β V |
45 | | vex 3442 |
. . . . . . . 8
β’ π¦ β V |
46 | 44, 45 | xpex 7632 |
. . . . . . 7
β’ (π₯ Γ π¦) β V |
47 | 43, 46 | elrnmpo 7439 |
. . . . . 6
β’
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β ran (π₯ β ran (,), π¦ β ran (,) β¦ (π₯ Γ π¦)) β βπ₯ β ran (,)βπ¦ β ran (,)((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) = (π₯ Γ π¦)) |
48 | 42, 47 | sylibr 234 |
. . . . 5
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β ran (π₯ β ran (,), π¦ β ran (,) β¦ (π₯ Γ π¦))) |
49 | | tpr2rico.2 |
. . . . 5
β’ π΅ = ran (π₯ β ran (,), π¦ β ran (,) β¦ (π₯ Γ π¦)) |
50 | 48, 49 | eleqtrrdi 2848 |
. . . 4
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΅) |
51 | 50 | ralrimiva 3140 |
. . 3
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΅) |
52 | | xpss 5613 |
. . . . . . 7
β’ (β
Γ β) β (V Γ V) |
53 | 52, 16 | sselid 3925 |
. . . . . 6
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β π β (V Γ
V)) |
54 | 18 | rexrd 11068 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(1st βπ)
β β*) |
55 | 19 | rphalfcld 12827 |
. . . . . . . . 9
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β (π / 2) β
β+) |
56 | 18, 55 | ltsubrpd 12847 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((1st βπ)
β (π / 2)) <
(1st βπ)) |
57 | 18, 55 | ltaddrpd 12848 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(1st βπ)
< ((1st βπ) + (π / 2))) |
58 | | elioo1 13162 |
. . . . . . . . 9
β’
((((1st βπ) β (π / 2)) β β* β§
((1st βπ)
+ (π / 2)) β
β*) β ((1st βπ) β (((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) β ((1st βπ) β β*
β§ ((1st βπ) β (π / 2)) < (1st βπ) β§ (1st
βπ) <
((1st βπ)
+ (π /
2))))) |
59 | 23, 25, 58 | syl2anc 585 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((1st βπ)
β (((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) β ((1st βπ) β β*
β§ ((1st βπ) β (π / 2)) < (1st βπ) β§ (1st
βπ) <
((1st βπ)
+ (π /
2))))) |
60 | 54, 56, 57, 59 | mpbir3and 1342 |
. . . . . . 7
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(1st βπ)
β (((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2)))) |
61 | 29 | rexrd 11068 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(2nd βπ)
β β*) |
62 | 29, 55 | ltsubrpd 12847 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((2nd βπ)
β (π / 2)) <
(2nd βπ)) |
63 | 29, 55 | ltaddrpd 12848 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(2nd βπ)
< ((2nd βπ) + (π / 2))) |
64 | | elioo1 13162 |
. . . . . . . . 9
β’
((((2nd βπ) β (π / 2)) β β* β§
((2nd βπ)
+ (π / 2)) β
β*) β ((2nd βπ) β (((2nd βπ) β (π / 2))(,)((2nd βπ) + (π / 2))) β ((2nd βπ) β β*
β§ ((2nd βπ) β (π / 2)) < (2nd βπ) β§ (2nd
βπ) <
((2nd βπ)
+ (π /
2))))) |
65 | 31, 33, 64 | syl2anc 585 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((2nd βπ)
β (((2nd βπ) β (π / 2))(,)((2nd βπ) + (π / 2))) β ((2nd βπ) β β*
β§ ((2nd βπ) β (π / 2)) < (2nd βπ) β§ (2nd
βπ) <
((2nd βπ)
+ (π /
2))))) |
66 | 61, 62, 63, 65 | mpbir3and 1342 |
. . . . . . 7
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(2nd βπ)
β (((2nd βπ) β (π / 2))(,)((2nd βπ) + (π / 2)))) |
67 | 60, 66 | jca 513 |
. . . . . 6
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((1st βπ)
β (((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) β§ (2nd βπ) β (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2))))) |
68 | | elxp7 7895 |
. . . . . 6
β’ (π β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β (π β (V Γ V) β§ ((1st
βπ) β
(((1st βπ)
β (π /
2))(,)((1st βπ) + (π / 2))) β§ (2nd βπ) β (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))))) |
69 | 53, 67, 68 | sylanbrc 584 |
. . . . 5
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β π β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))))) |
70 | 69 | ralrimiva 3140 |
. . . 4
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+ π β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2))))) |
71 | | mnfle 12913 |
. . . . . . . . . . . . . . . . . 18
β’
(((1st βπ) β (π / 2)) β β* β
-β β€ ((1st βπ) β (π / 2))) |
72 | 23, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β -β
β€ ((1st βπ) β (π / 2))) |
73 | | pnfge 12909 |
. . . . . . . . . . . . . . . . . 18
β’
(((1st βπ) + (π / 2)) β β* β
((1st βπ)
+ (π / 2)) β€
+β) |
74 | 25, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((1st βπ)
+ (π / 2)) β€
+β) |
75 | | mnfxr 11075 |
. . . . . . . . . . . . . . . . . 18
β’ -β
β β* |
76 | | pnfxr 11072 |
. . . . . . . . . . . . . . . . . 18
β’ +β
β β* |
77 | | ioossioo 13216 |
. . . . . . . . . . . . . . . . . 18
β’
(((-β β β* β§ +β β
β*) β§ (-β β€ ((1st βπ) β (π / 2)) β§ ((1st βπ) + (π / 2)) β€ +β)) β
(((1st βπ)
β (π /
2))(,)((1st βπ) + (π / 2))) β
(-β(,)+β)) |
78 | 75, 76, 77 | mpanl12 700 |
. . . . . . . . . . . . . . . . 17
β’
((-β β€ ((1st βπ) β (π / 2)) β§ ((1st βπ) + (π / 2)) β€ +β) β
(((1st βπ)
β (π /
2))(,)((1st βπ) + (π / 2))) β
(-β(,)+β)) |
79 | 72, 74, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(((1st βπ)
β (π /
2))(,)((1st βπ) + (π / 2))) β
(-β(,)+β)) |
80 | | ioomax 13197 |
. . . . . . . . . . . . . . . 16
β’
(-β(,)+β) = β |
81 | 79, 80 | sseqtrdi 3977 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(((1st βπ)
β (π /
2))(,)((1st βπ) + (π / 2))) β β) |
82 | | mnfle 12913 |
. . . . . . . . . . . . . . . . . 18
β’
(((2nd βπ) β (π / 2)) β β* β
-β β€ ((2nd βπ) β (π / 2))) |
83 | 31, 82 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β -β
β€ ((2nd βπ) β (π / 2))) |
84 | | pnfge 12909 |
. . . . . . . . . . . . . . . . . 18
β’
(((2nd βπ) + (π / 2)) β β* β
((2nd βπ)
+ (π / 2)) β€
+β) |
85 | 33, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((2nd βπ)
+ (π / 2)) β€
+β) |
86 | | ioossioo 13216 |
. . . . . . . . . . . . . . . . . 18
β’
(((-β β β* β§ +β β
β*) β§ (-β β€ ((2nd βπ) β (π / 2)) β§ ((2nd βπ) + (π / 2)) β€ +β)) β
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))) β
(-β(,)+β)) |
87 | 75, 76, 86 | mpanl12 700 |
. . . . . . . . . . . . . . . . 17
β’
((-β β€ ((2nd βπ) β (π / 2)) β§ ((2nd βπ) + (π / 2)) β€ +β) β
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))) β
(-β(,)+β)) |
88 | 83, 85, 87 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))) β
(-β(,)+β)) |
89 | 88, 80 | sseqtrdi 3977 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))) β β) |
90 | | xpss12 5612 |
. . . . . . . . . . . . . . 15
β’
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) β β β§
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))) β β) β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β
Γ β)) |
91 | 81, 89, 90 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β
Γ β)) |
92 | 91 | sselda 3927 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))))) β π₯ β (β Γ
β)) |
93 | 92 | expcom 415 |
. . . . . . . . . . . 12
β’ (π₯ β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β π₯ β (β Γ
β))) |
94 | 93 | ancld 552 |
. . . . . . . . . . 11
β’ (π₯ β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)))) |
95 | 94 | imdistanri 571 |
. . . . . . . . . 10
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))))) β ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ π₯ β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))))) |
96 | 13 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β (π½ Γt π½) β§ (π β π΄ β§ π β β+ β§ π₯ β (β Γ
β))) β π΄ β
(β Γ β)) |
97 | | simpr1 1194 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β (π½ Γt π½) β§ (π β π΄ β§ π β β+ β§ π₯ β (β Γ
β))) β π β
π΄) |
98 | 96, 97 | sseldd 3928 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β (π½ Γt π½) β§ (π β π΄ β§ π β β+ β§ π₯ β (β Γ
β))) β π β
(β Γ β)) |
99 | 98 | 3anassrs 1360 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β π β
(β Γ β)) |
100 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β π₯ β
(β Γ β)) |
101 | | simplr 767 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β π β
β+) |
102 | 101 | rphalfcld 12827 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (π / 2)
β β+) |
103 | | tpr2rico.1 |
. . . . . . . . . . . . . . 15
β’ πΊ = (π’ β β, π£ β β β¦ (π’ + (i Β· π£))) |
104 | 103 | cnre2csqima 31903 |
. . . . . . . . . . . . . 14
β’ ((π β (β Γ
β) β§ π₯ β
(β Γ β) β§ (π / 2) β β+) β
(π₯ β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β
((absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2) β§ (absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2)))) |
105 | 99, 100, 102, 104 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (π₯ β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β
((absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2) β§ (absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2)))) |
106 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(TopOpenββfld) =
(TopOpenββfld) |
107 | 103, 6, 106 | cnrehmeo 24158 |
. . . . . . . . . . . . . . . . . . . 20
β’ πΊ β ((π½ Γt π½)Homeo(TopOpenββfld)) |
108 | 106 | cnfldtopon 23988 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(TopOpenββfld) β
(TopOnββ) |
109 | 108 | toponunii 22107 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β =
βͺ
(TopOpenββfld) |
110 | 12, 109 | hmeof1o 22957 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΊ β ((π½ Γt π½)Homeo(TopOpenββfld))
β πΊ:(β Γ
β)β1-1-ontoββ) |
111 | | f1of 6743 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΊ:(β Γ
β)β1-1-ontoββ β πΊ:(β Γ
β)βΆβ) |
112 | 107, 110,
111 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
β’ πΊ:(β Γ
β)βΆβ |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β πΊ:(β
Γ β)βΆβ) |
114 | 113, 99 | ffvelcdmd 6991 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (πΊβπ) β β) |
115 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β πΊ:(β Γ
β)βΆβ) |
116 | 115 | ffvelcdmda 6990 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (πΊβπ₯) β β) |
117 | | sqsscirc2 31901 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊβπ) β β β§ (πΊβπ₯) β β) β§ π β β+) β
(((absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2) β§ (absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2)) β (absβ((πΊβπ₯) β (πΊβπ))) < π)) |
118 | 114, 116,
101, 117 | syl21anc 836 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (((absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2) β§ (absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2)) β (absβ((πΊβπ₯) β (πΊβπ))) < π)) |
119 | 118 | imp 408 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ ((absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2) β§ (absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2))) β (absβ((πΊβπ₯) β (πΊβπ))) < π) |
120 | 101 | rpxrd 12816 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β π β
β*) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β π β β*) |
122 | | cnxmet 23978 |
. . . . . . . . . . . . . . . . 17
β’ (abs
β β ) β (βMetββ) |
123 | 121, 122 | jctil 521 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β ((abs β β ) β
(βMetββ) β§ π β
β*)) |
124 | 114 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β (πΊβπ) β β) |
125 | 116 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β (πΊβπ₯) β β) |
126 | 124, 125 | jca 513 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β ((πΊβπ) β β β§ (πΊβπ₯) β β)) |
127 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . 19
β’ (abs
β β ) = (abs β β ) |
128 | 127 | cnmetdval 23976 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΊβπ₯) β β β§ (πΊβπ) β β) β ((πΊβπ₯)(abs β β )(πΊβπ)) = (absβ((πΊβπ₯) β (πΊβπ)))) |
129 | 125, 124,
128 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β ((πΊβπ₯)(abs β β )(πΊβπ)) = (absβ((πΊβπ₯) β (πΊβπ)))) |
130 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β (absβ((πΊβπ₯) β (πΊβπ))) < π) |
131 | 129, 130 | eqbrtrd 5104 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β ((πΊβπ₯)(abs β β )(πΊβπ)) < π) |
132 | | elbl3 23587 |
. . . . . . . . . . . . . . . . 17
β’ ((((abs
β β ) β (βMetββ) β§ π β β*) β§ ((πΊβπ) β β β§ (πΊβπ₯) β β)) β ((πΊβπ₯) β ((πΊβπ)(ballβ(abs β β ))π) β ((πΊβπ₯)(abs β β )(πΊβπ)) < π)) |
133 | 132 | biimpar 479 |
. . . . . . . . . . . . . . . 16
β’ (((((abs
β β ) β (βMetββ) β§ π β β*) β§ ((πΊβπ) β β β§ (πΊβπ₯) β β)) β§ ((πΊβπ₯)(abs β β )(πΊβπ)) < π) β (πΊβπ₯) β ((πΊβπ)(ballβ(abs β β ))π)) |
134 | 123, 126,
131, 133 | syl21anc 836 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ (absβ((πΊβπ₯) β (πΊβπ))) < π) β (πΊβπ₯) β ((πΊβπ)(ballβ(abs β β ))π)) |
135 | 119, 134 | syldan 592 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ ((absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2) β§ (absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2))) β (πΊβπ₯) β ((πΊβπ)(ballβ(abs β β ))π)) |
136 | 135 | ex 414 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (((absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2) β§ (absβ(ββ((πΊβπ₯) β (πΊβπ)))) < (π / 2)) β (πΊβπ₯) β ((πΊβπ)(ballβ(abs β β ))π))) |
137 | 105, 136 | syld 47 |
. . . . . . . . . . . 12
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (π₯ β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (πΊβπ₯) β ((πΊβπ)(ballβ(abs β β ))π))) |
138 | | f1ocnv 6755 |
. . . . . . . . . . . . . . 15
β’ (πΊ:(β Γ
β)β1-1-ontoββ β β‘πΊ:ββ1-1-ontoβ(β Γ β)) |
139 | 107, 110,
138 | mp2b 10 |
. . . . . . . . . . . . . 14
β’ β‘πΊ:ββ1-1-ontoβ(β Γ β) |
140 | | f1ofun 6745 |
. . . . . . . . . . . . . 14
β’ (β‘πΊ:ββ1-1-ontoβ(β Γ β) β Fun β‘πΊ) |
141 | 139, 140 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ Fun β‘πΊ |
142 | | f1odm 6747 |
. . . . . . . . . . . . . . 15
β’ (β‘πΊ:ββ1-1-ontoβ(β Γ β) β dom β‘πΊ = β) |
143 | 139, 142 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ dom β‘πΊ = β |
144 | 116, 143 | eleqtrrdi 2848 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (πΊβπ₯) β dom β‘πΊ) |
145 | | funfvima 7135 |
. . . . . . . . . . . . 13
β’ ((Fun
β‘πΊ β§ (πΊβπ₯) β dom β‘πΊ) β ((πΊβπ₯) β ((πΊβπ)(ballβ(abs β β ))π) β (β‘πΊβ(πΊβπ₯)) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)))) |
146 | 141, 144,
145 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β ((πΊβπ₯) β ((πΊβπ)(ballβ(abs β β ))π) β (β‘πΊβ(πΊβπ₯)) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)))) |
147 | 107, 110 | mp1i 13 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β πΊ:(β
Γ β)β1-1-ontoββ) |
148 | | f1ocnvfv1 7177 |
. . . . . . . . . . . . . . 15
β’ ((πΊ:(β Γ
β)β1-1-ontoββ β§ π₯ β (β Γ β)) β
(β‘πΊβ(πΊβπ₯)) = π₯) |
149 | 147, 100,
148 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (β‘πΊβ(πΊβπ₯)) = π₯) |
150 | 149 | eleq1d 2821 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β ((β‘πΊβ(πΊβπ₯)) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π₯ β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)))) |
151 | 150 | biimpd 228 |
. . . . . . . . . . . 12
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β ((β‘πΊβ(πΊβπ₯)) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π₯ β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)))) |
152 | 137, 146,
151 | 3syld 60 |
. . . . . . . . . . 11
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β (π₯ β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π₯ β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)))) |
153 | 152 | imp 408 |
. . . . . . . . . 10
β’
(((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β (β Γ
β)) β§ π₯ β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2))))) β π₯ β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π))) |
154 | 95, 153 | syl 17 |
. . . . . . . . 9
β’ ((((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β§ π₯ β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2))))) β π₯ β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π))) |
155 | 154 | ex 414 |
. . . . . . . 8
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β (π₯ β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β π₯ β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)))) |
156 | 155 | ssrdv 3933 |
. . . . . . 7
β’ (((π΄ β (π½ Γt π½) β§ π β π΄) β§ π β β+) β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π))) |
157 | 156 | ralrimiva 3140 |
. . . . . 6
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π))) |
158 | 103 | mpofun 7427 |
. . . . . . . . . 10
β’ Fun πΊ |
159 | 158 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β Fun πΊ) |
160 | 13 | sselda 3927 |
. . . . . . . . . 10
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β π β (β Γ
β)) |
161 | | f1odm 6747 |
. . . . . . . . . . 11
β’ (πΊ:(β Γ
β)β1-1-ontoββ β dom πΊ = (β Γ
β)) |
162 | 107, 110,
161 | mp2b 10 |
. . . . . . . . . 10
β’ dom πΊ = (β Γ
β) |
163 | 160, 162 | eleqtrrdi 2848 |
. . . . . . . . 9
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β π β dom πΊ) |
164 | | simpr 486 |
. . . . . . . . 9
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β π β π΄) |
165 | | funfvima 7135 |
. . . . . . . . . 10
β’ ((Fun
πΊ β§ π β dom πΊ) β (π β π΄ β (πΊβπ) β (πΊ β π΄))) |
166 | 165 | imp 408 |
. . . . . . . . 9
β’ (((Fun
πΊ β§ π β dom πΊ) β§ π β π΄) β (πΊβπ) β (πΊ β π΄)) |
167 | 159, 163,
164, 166 | syl21anc 836 |
. . . . . . . 8
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β (πΊβπ) β (πΊ β π΄)) |
168 | | hmeoima 22958 |
. . . . . . . . . . 11
β’ ((πΊ β ((π½ Γt π½)Homeo(TopOpenββfld))
β§ π΄ β (π½ Γt π½)) β (πΊ β π΄) β
(TopOpenββfld)) |
169 | 107, 168 | mpan 688 |
. . . . . . . . . 10
β’ (π΄ β (π½ Γt π½) β (πΊ β π΄) β
(TopOpenββfld)) |
170 | 106 | cnfldtopn 23987 |
. . . . . . . . . . . . 13
β’
(TopOpenββfld) = (MetOpenβ(abs β
β )) |
171 | 170 | elmopn2 23640 |
. . . . . . . . . . . 12
β’ ((abs
β β ) β (βMetββ) β ((πΊ β π΄) β
(TopOpenββfld) β ((πΊ β π΄) β β β§ βπ β (πΊ β π΄)βπ β β+ (π(ballβ(abs β β
))π) β (πΊ β π΄)))) |
172 | 122, 171 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((πΊ β π΄) β
(TopOpenββfld) β ((πΊ β π΄) β β β§ βπ β (πΊ β π΄)βπ β β+ (π(ballβ(abs β β
))π) β (πΊ β π΄))) |
173 | 172 | simprbi 498 |
. . . . . . . . . 10
β’ ((πΊ β π΄) β
(TopOpenββfld) β βπ β (πΊ β π΄)βπ β β+ (π(ballβ(abs β β
))π) β (πΊ β π΄)) |
174 | 169, 173 | syl 17 |
. . . . . . . . 9
β’ (π΄ β (π½ Γt π½) β βπ β (πΊ β π΄)βπ β β+ (π(ballβ(abs β β
))π) β (πΊ β π΄)) |
175 | 174 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β (πΊ β π΄)βπ β β+ (π(ballβ(abs β β
))π) β (πΊ β π΄)) |
176 | | oveq1 7311 |
. . . . . . . . . . 11
β’ (π = (πΊβπ) β (π(ballβ(abs β β ))π) = ((πΊβπ)(ballβ(abs β β ))π)) |
177 | 176 | sseq1d 3958 |
. . . . . . . . . 10
β’ (π = (πΊβπ) β ((π(ballβ(abs β β ))π) β (πΊ β π΄) β ((πΊβπ)(ballβ(abs β β ))π) β (πΊ β π΄))) |
178 | 177 | rexbidv 3172 |
. . . . . . . . 9
β’ (π = (πΊβπ) β (βπ β β+ (π(ballβ(abs β β
))π) β (πΊ β π΄) β βπ β β+ ((πΊβπ)(ballβ(abs β β ))π) β (πΊ β π΄))) |
179 | 178 | rspcva 3565 |
. . . . . . . 8
β’ (((πΊβπ) β (πΊ β π΄) β§ βπ β (πΊ β π΄)βπ β β+ (π(ballβ(abs β β
))π) β (πΊ β π΄)) β βπ β β+ ((πΊβπ)(ballβ(abs β β ))π) β (πΊ β π΄)) |
180 | 167, 175,
179 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+ ((πΊβπ)(ballβ(abs β β ))π) β (πΊ β π΄)) |
181 | | imass2 6017 |
. . . . . . . . . 10
β’ (((πΊβπ)(ballβ(abs β β ))π) β (πΊ β π΄) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β (β‘πΊ β (πΊ β π΄))) |
182 | | f1of1 6742 |
. . . . . . . . . . . . 13
β’ (πΊ:(β Γ
β)β1-1-ontoββ β πΊ:(β Γ β)β1-1ββ) |
183 | 107, 110,
182 | mp2b 10 |
. . . . . . . . . . . 12
β’ πΊ:(β Γ
β)β1-1ββ |
184 | | f1imacnv 6759 |
. . . . . . . . . . . 12
β’ ((πΊ:(β Γ
β)β1-1ββ β§
π΄ β (β Γ
β)) β (β‘πΊ β (πΊ β π΄)) = π΄) |
185 | 183, 13, 184 | sylancr 588 |
. . . . . . . . . . 11
β’ (π΄ β (π½ Γt π½) β (β‘πΊ β (πΊ β π΄)) = π΄) |
186 | 185 | sseq2d 3959 |
. . . . . . . . . 10
β’ (π΄ β (π½ Γt π½) β ((β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β (β‘πΊ β (πΊ β π΄)) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄)) |
187 | 181, 186 | syl5ib 245 |
. . . . . . . . 9
β’ (π΄ β (π½ Γt π½) β (((πΊβπ)(ballβ(abs β β ))π) β (πΊ β π΄) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄)) |
188 | 187 | reximdv 3164 |
. . . . . . . 8
β’ (π΄ β (π½ Γt π½) β (βπ β β+ ((πΊβπ)(ballβ(abs β β ))π) β (πΊ β π΄) β βπ β β+ (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄)) |
189 | 188 | adantr 482 |
. . . . . . 7
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β (βπ β β+ ((πΊβπ)(ballβ(abs β β ))π) β (πΊ β π΄) β βπ β β+ (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄)) |
190 | 180, 189 | mpd 15 |
. . . . . 6
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+ (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄) |
191 | | r19.29 3114 |
. . . . . 6
β’
((βπ β
β+ ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β§ βπ β β+
(β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄) β βπ β β+
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β§ (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄)) |
192 | 157, 190,
191 | syl2anc 585 |
. . . . 5
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β§ (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄)) |
193 | | sstr 3935 |
. . . . . 6
β’
((((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β§ (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄) β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄) |
194 | 193 | reximi 3084 |
. . . . 5
β’
(βπ β
β+ (((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β§ (β‘πΊ β ((πΊβπ)(ballβ(abs β β ))π)) β π΄) β βπ β β+
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄) |
195 | 192, 194 | syl 17 |
. . . 4
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄) |
196 | | r19.29 3114 |
. . . 4
β’
((βπ β
β+ π
β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β§ βπ β β+
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄) β βπ β β+
(π β
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β§
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄)) |
197 | 70, 195, 196 | syl2anc 585 |
. . 3
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+ (π β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β§ ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β π΄)) |
198 | | r19.29 3114 |
. . 3
β’
((βπ β
β+ ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΅ β§ βπ β β+ (π β ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β§ ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β π΄)) β βπ β β+
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΅ β§ (π β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β§
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄))) |
199 | 51, 197, 198 | syl2anc 585 |
. 2
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β β+
(((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΅ β§ (π β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β§
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄))) |
200 | | eleq2 2825 |
. . . . 5
β’ (π = ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β (π β π β π β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))))) |
201 | | sseq1 3952 |
. . . . 5
β’ (π = ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β (π β π΄ β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄)) |
202 | 200, 201 | anbi12d 632 |
. . . 4
β’ (π = ((((1st
βπ) β (π / 2))(,)((1st
βπ) + (π / 2))) Γ
(((2nd βπ)
β (π /
2))(,)((2nd βπ) + (π / 2)))) β ((π β π β§ π β π΄) β (π β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β§
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄))) |
203 | 202 | rspcev 3567 |
. . 3
β’
((((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΅ β§ (π β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β§
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄)) β βπ β π΅ (π β π β§ π β π΄)) |
204 | 203 | rexlimivw 3145 |
. 2
β’
(βπ β
β+ (((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΅ β§ (π β ((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β§
((((1st βπ) β (π / 2))(,)((1st βπ) + (π / 2))) Γ (((2nd
βπ) β (π / 2))(,)((2nd
βπ) + (π / 2)))) β π΄)) β βπ β π΅ (π β π β§ π β π΄)) |
205 | 199, 204 | syl 17 |
1
β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β π΅ (π β π β§ π β π΄)) |