Step | Hyp | Ref
| Expression |
1 | | iccssxr 13276 |
. . . 4
β’ (-1[,]1)
β β* |
2 | | xrltso 12989 |
. . . 4
β’ < Or
β* |
3 | | soss 5563 |
. . . 4
β’ ((-1[,]1)
β β* β ( < Or β* β < Or
(-1[,]1))) |
4 | 1, 2, 3 | mp2 9 |
. . 3
β’ < Or
(-1[,]1) |
5 | | sopo 5562 |
. . . 4
β’ ( < Or
β* β < Po β*) |
6 | 2, 5 | ax-mp 5 |
. . 3
β’ < Po
β* |
7 | | xrhmeo.g |
. . . . 5
β’ πΊ = (π¦ β (-1[,]1) β¦ if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
8 | | iccssxr 13276 |
. . . . . . 7
β’
(0[,]+β) β β* |
9 | | neg1rr 12202 |
. . . . . . . . . . . 12
β’ -1 β
β |
10 | | 1re 11089 |
. . . . . . . . . . . 12
β’ 1 β
β |
11 | 9, 10 | elicc2i 13259 |
. . . . . . . . . . 11
β’ (π¦ β (-1[,]1) β (π¦ β β β§ -1 β€
π¦ β§ π¦ β€ 1)) |
12 | 11 | simp1bi 1146 |
. . . . . . . . . 10
β’ (π¦ β (-1[,]1) β π¦ β
β) |
13 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π¦ β (-1[,]1) β§ 0 β€
π¦) β π¦ β
β) |
14 | | simpr 486 |
. . . . . . . . 9
β’ ((π¦ β (-1[,]1) β§ 0 β€
π¦) β 0 β€ π¦) |
15 | 11 | simp3bi 1148 |
. . . . . . . . . 10
β’ (π¦ β (-1[,]1) β π¦ β€ 1) |
16 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((π¦ β (-1[,]1) β§ 0 β€
π¦) β π¦ β€ 1) |
17 | | elicc01 13312 |
. . . . . . . . 9
β’ (π¦ β (0[,]1) β (π¦ β β β§ 0 β€
π¦ β§ π¦ β€ 1)) |
18 | 13, 14, 16, 17 | syl3anbrc 1344 |
. . . . . . . 8
β’ ((π¦ β (-1[,]1) β§ 0 β€
π¦) β π¦ β
(0[,]1)) |
19 | | xrhmeo.f |
. . . . . . . . . . . 12
β’ πΉ = (π₯ β (0[,]1) β¦ if(π₯ = 1, +β, (π₯ / (1 β π₯)))) |
20 | 19 | iccpnfcnv 24229 |
. . . . . . . . . . 11
β’ (πΉ:(0[,]1)β1-1-ontoβ(0[,]+β) β§ β‘πΉ = (π£ β (0[,]+β) β¦ if(π£ = +β, 1, (π£ / (1 + π£))))) |
21 | 20 | simpli 485 |
. . . . . . . . . 10
β’ πΉ:(0[,]1)β1-1-ontoβ(0[,]+β) |
22 | | f1of 6780 |
. . . . . . . . . 10
β’ (πΉ:(0[,]1)β1-1-ontoβ(0[,]+β) β πΉ:(0[,]1)βΆ(0[,]+β)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . 9
β’ πΉ:(0[,]1)βΆ(0[,]+β) |
24 | 23 | ffvelcdmi 7029 |
. . . . . . . 8
β’ (π¦ β (0[,]1) β (πΉβπ¦) β (0[,]+β)) |
25 | 18, 24 | syl 17 |
. . . . . . 7
β’ ((π¦ β (-1[,]1) β§ 0 β€
π¦) β (πΉβπ¦) β (0[,]+β)) |
26 | 8, 25 | sselid 3941 |
. . . . . 6
β’ ((π¦ β (-1[,]1) β§ 0 β€
π¦) β (πΉβπ¦) β
β*) |
27 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β π¦ β
β) |
28 | 27 | renegcld 11516 |
. . . . . . . . . 10
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β -π¦ β
β) |
29 | | 0re 11091 |
. . . . . . . . . . . . 13
β’ 0 β
β |
30 | | letric 11189 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ π¦
β β) β (0 β€ π¦ β¨ π¦ β€ 0)) |
31 | 29, 12, 30 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π¦ β (-1[,]1) β (0 β€
π¦ β¨ π¦ β€ 0)) |
32 | 31 | orcanai 1002 |
. . . . . . . . . . 11
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β π¦ β€ 0) |
33 | 27 | le0neg1d 11660 |
. . . . . . . . . . 11
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β (π¦ β€ 0 β 0 β€ -π¦)) |
34 | 32, 33 | mpbid 231 |
. . . . . . . . . 10
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β 0 β€
-π¦) |
35 | 11 | simp2bi 1147 |
. . . . . . . . . . . 12
β’ (π¦ β (-1[,]1) β -1 β€
π¦) |
36 | 35 | adantr 482 |
. . . . . . . . . . 11
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β -1 β€
π¦) |
37 | | lenegcon1 11593 |
. . . . . . . . . . . 12
β’ ((1
β β β§ π¦
β β) β (-1 β€ π¦ β -π¦ β€ 1)) |
38 | 10, 27, 37 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β (-1 β€
π¦ β -π¦ β€ 1)) |
39 | 36, 38 | mpbid 231 |
. . . . . . . . . 10
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β -π¦ β€ 1) |
40 | | elicc01 13312 |
. . . . . . . . . 10
β’ (-π¦ β (0[,]1) β (-π¦ β β β§ 0 β€
-π¦ β§ -π¦ β€ 1)) |
41 | 28, 34, 39, 40 | syl3anbrc 1344 |
. . . . . . . . 9
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β -π¦ β
(0[,]1)) |
42 | 23 | ffvelcdmi 7029 |
. . . . . . . . 9
β’ (-π¦ β (0[,]1) β (πΉβ-π¦) β (0[,]+β)) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β (πΉβ-π¦) β (0[,]+β)) |
44 | 8, 43 | sselid 3941 |
. . . . . . 7
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β (πΉβ-π¦) β
β*) |
45 | 44 | xnegcld 13148 |
. . . . . 6
β’ ((π¦ β (-1[,]1) β§ Β¬ 0
β€ π¦) β
-π(πΉβ-π¦) β
β*) |
46 | 26, 45 | ifclda 4520 |
. . . . 5
β’ (π¦ β (-1[,]1) β if(0
β€ π¦, (πΉβπ¦), -π(πΉβ-π¦)) β
β*) |
47 | 7, 46 | fmpti 7055 |
. . . 4
β’ πΊ:(-1[,]1)βΆβ* |
48 | | frn 6671 |
. . . . . 6
β’ (πΊ:(-1[,]1)βΆβ* β
ran πΊ β
β*) |
49 | 47, 48 | ax-mp 5 |
. . . . 5
β’ ran πΊ β
β* |
50 | | ssabral 4018 |
. . . . . . 7
β’
(β* β {π§ β£ βπ¦ β (-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))} β βπ§ β β* βπ¦ β (-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
51 | | 0le1 11612 |
. . . . . . . . . . . . 13
β’ 0 β€
1 |
52 | | le0neg2 11598 |
. . . . . . . . . . . . . 14
β’ (1 β
β β (0 β€ 1 β -1 β€ 0)) |
53 | 10, 52 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (0 β€ 1
β -1 β€ 0) |
54 | 51, 53 | mpbi 229 |
. . . . . . . . . . . 12
β’ -1 β€
0 |
55 | | 1le1 11717 |
. . . . . . . . . . . 12
β’ 1 β€
1 |
56 | | iccss 13261 |
. . . . . . . . . . . 12
β’ (((-1
β β β§ 1 β β) β§ (-1 β€ 0 β§ 1 β€ 1)) β
(0[,]1) β (-1[,]1)) |
57 | 9, 10, 54, 55, 56 | mp4an 692 |
. . . . . . . . . . 11
β’ (0[,]1)
β (-1[,]1) |
58 | | elxrge0 13303 |
. . . . . . . . . . . 12
β’ (π§ β (0[,]+β) β
(π§ β
β* β§ 0 β€ π§)) |
59 | | f1ocnv 6792 |
. . . . . . . . . . . . . 14
β’ (πΉ:(0[,]1)β1-1-ontoβ(0[,]+β) β β‘πΉ:(0[,]+β)β1-1-ontoβ(0[,]1)) |
60 | | f1of 6780 |
. . . . . . . . . . . . . 14
β’ (β‘πΉ:(0[,]+β)β1-1-ontoβ(0[,]1) β β‘πΉ:(0[,]+β)βΆ(0[,]1)) |
61 | 21, 59, 60 | mp2b 10 |
. . . . . . . . . . . . 13
β’ β‘πΉ:(0[,]+β)βΆ(0[,]1) |
62 | 61 | ffvelcdmi 7029 |
. . . . . . . . . . . 12
β’ (π§ β (0[,]+β) β
(β‘πΉβπ§) β (0[,]1)) |
63 | 58, 62 | sylbir 234 |
. . . . . . . . . . 11
β’ ((π§ β β*
β§ 0 β€ π§) β
(β‘πΉβπ§) β (0[,]1)) |
64 | 57, 63 | sselid 3941 |
. . . . . . . . . 10
β’ ((π§ β β*
β§ 0 β€ π§) β
(β‘πΉβπ§) β (-1[,]1)) |
65 | | elicc01 13312 |
. . . . . . . . . . . 12
β’ ((β‘πΉβπ§) β (0[,]1) β ((β‘πΉβπ§) β β β§ 0 β€ (β‘πΉβπ§) β§ (β‘πΉβπ§) β€ 1)) |
66 | 65 | simp2bi 1147 |
. . . . . . . . . . 11
β’ ((β‘πΉβπ§) β (0[,]1) β 0 β€ (β‘πΉβπ§)) |
67 | 63, 66 | syl 17 |
. . . . . . . . . 10
β’ ((π§ β β*
β§ 0 β€ π§) β 0
β€ (β‘πΉβπ§)) |
68 | 58 | biimpri 227 |
. . . . . . . . . . . 12
β’ ((π§ β β*
β§ 0 β€ π§) β
π§ β
(0[,]+β)) |
69 | | f1ocnvfv2 7218 |
. . . . . . . . . . . 12
β’ ((πΉ:(0[,]1)β1-1-ontoβ(0[,]+β) β§ π§ β (0[,]+β)) β (πΉβ(β‘πΉβπ§)) = π§) |
70 | 21, 68, 69 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π§ β β*
β§ 0 β€ π§) β
(πΉβ(β‘πΉβπ§)) = π§) |
71 | 70 | eqcomd 2744 |
. . . . . . . . . 10
β’ ((π§ β β*
β§ 0 β€ π§) β
π§ = (πΉβ(β‘πΉβπ§))) |
72 | | breq2 5108 |
. . . . . . . . . . . 12
β’ (π¦ = (β‘πΉβπ§) β (0 β€ π¦ β 0 β€ (β‘πΉβπ§))) |
73 | | fveq2 6838 |
. . . . . . . . . . . . 13
β’ (π¦ = (β‘πΉβπ§) β (πΉβπ¦) = (πΉβ(β‘πΉβπ§))) |
74 | 73 | eqeq2d 2749 |
. . . . . . . . . . . 12
β’ (π¦ = (β‘πΉβπ§) β (π§ = (πΉβπ¦) β π§ = (πΉβ(β‘πΉβπ§)))) |
75 | 72, 74 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π¦ = (β‘πΉβπ§) β ((0 β€ π¦ β§ π§ = (πΉβπ¦)) β (0 β€ (β‘πΉβπ§) β§ π§ = (πΉβ(β‘πΉβπ§))))) |
76 | 75 | rspcev 3580 |
. . . . . . . . . 10
β’ (((β‘πΉβπ§) β (-1[,]1) β§ (0 β€ (β‘πΉβπ§) β§ π§ = (πΉβ(β‘πΉβπ§)))) β βπ¦ β (-1[,]1)(0 β€ π¦ β§ π§ = (πΉβπ¦))) |
77 | 64, 67, 71, 76 | syl12anc 836 |
. . . . . . . . 9
β’ ((π§ β β*
β§ 0 β€ π§) β
βπ¦ β (-1[,]1)(0
β€ π¦ β§ π§ = (πΉβπ¦))) |
78 | | iftrue 4491 |
. . . . . . . . . . . 12
β’ (0 β€
π¦ β if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦)) = (πΉβπ¦)) |
79 | 78 | eqeq2d 2749 |
. . . . . . . . . . 11
β’ (0 β€
π¦ β (π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦)) β π§ = (πΉβπ¦))) |
80 | 79 | biimpar 479 |
. . . . . . . . . 10
β’ ((0 β€
π¦ β§ π§ = (πΉβπ¦)) β π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
81 | 80 | reximi 3086 |
. . . . . . . . 9
β’
(βπ¦ β
(-1[,]1)(0 β€ π¦ β§
π§ = (πΉβπ¦)) β βπ¦ β (-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
82 | 77, 81 | syl 17 |
. . . . . . . 8
β’ ((π§ β β*
β§ 0 β€ π§) β
βπ¦ β
(-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
83 | | xnegcl 13061 |
. . . . . . . . . . . . . . . 16
β’ (π§ β β*
β -ππ§ β β*) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β -ππ§ β β*) |
85 | | 0xr 11136 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β* |
86 | | xrletri 13001 |
. . . . . . . . . . . . . . . . . . 19
β’ ((0
β β* β§ π§ β β*) β (0 β€
π§ β¨ π§ β€ 0)) |
87 | 85, 86 | mpan 689 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β β*
β (0 β€ π§ β¨ π§ β€ 0)) |
88 | 87 | ord 863 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β β*
β (Β¬ 0 β€ π§
β π§ β€
0)) |
89 | | xle0neg1 13069 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β β*
β (π§ β€ 0 β 0
β€ -ππ§)) |
90 | 88, 89 | sylibd 238 |
. . . . . . . . . . . . . . . 16
β’ (π§ β β*
β (Β¬ 0 β€ π§
β 0 β€ -ππ§)) |
91 | 90 | imp 408 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β 0 β€ -ππ§) |
92 | | elxrge0 13303 |
. . . . . . . . . . . . . . 15
β’
(-ππ§ β (0[,]+β) β
(-ππ§
β β* β§ 0 β€ -ππ§)) |
93 | 84, 91, 92 | sylanbrc 584 |
. . . . . . . . . . . . . 14
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β -ππ§ β (0[,]+β)) |
94 | 61 | ffvelcdmi 7029 |
. . . . . . . . . . . . . 14
β’
(-ππ§ β (0[,]+β) β (β‘πΉβ-ππ§) β
(0[,]1)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (β‘πΉβ-ππ§) β
(0[,]1)) |
96 | 57, 95 | sselid 3941 |
. . . . . . . . . . . 12
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (β‘πΉβ-ππ§) β
(-1[,]1)) |
97 | | iccssre 13275 |
. . . . . . . . . . . . . . 15
β’ ((-1
β β β§ 1 β β) β (-1[,]1) β
β) |
98 | 9, 10, 97 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (-1[,]1)
β β |
99 | 98, 96 | sselid 3941 |
. . . . . . . . . . . . 13
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (β‘πΉβ-ππ§) β
β) |
100 | | iccneg 13318 |
. . . . . . . . . . . . . 14
β’ ((-1
β β β§ 1 β β β§ (β‘πΉβ-ππ§) β β) β ((β‘πΉβ-ππ§) β (-1[,]1) β -(β‘πΉβ-ππ§) β
(-1[,]--1))) |
101 | 9, 10, 100 | mp3an12 1452 |
. . . . . . . . . . . . 13
β’ ((β‘πΉβ-ππ§) β β β ((β‘πΉβ-ππ§) β (-1[,]1) β -(β‘πΉβ-ππ§) β
(-1[,]--1))) |
102 | 99, 101 | syl 17 |
. . . . . . . . . . . 12
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β ((β‘πΉβ-ππ§) β (-1[,]1) β -(β‘πΉβ-ππ§) β
(-1[,]--1))) |
103 | 96, 102 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β -(β‘πΉβ-ππ§) β
(-1[,]--1)) |
104 | | negneg1e1 12205 |
. . . . . . . . . . . 12
β’ --1 =
1 |
105 | 104 | oveq2i 7361 |
. . . . . . . . . . 11
β’
(-1[,]--1) = (-1[,]1) |
106 | 103, 105 | eleqtrdi 2849 |
. . . . . . . . . 10
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β -(β‘πΉβ-ππ§) β
(-1[,]1)) |
107 | | xle0neg2 13070 |
. . . . . . . . . . . . . . 15
β’ (π§ β β*
β (0 β€ π§ β
-ππ§ β€
0)) |
108 | 107 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π§ β β*
β (Β¬ 0 β€ π§
β Β¬ -ππ§ β€ 0)) |
109 | 108 | biimpa 478 |
. . . . . . . . . . . . 13
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β Β¬ -ππ§ β€ 0) |
110 | | f1ocnvfv2 7218 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:(0[,]1)β1-1-ontoβ(0[,]+β) β§
-ππ§
β (0[,]+β)) β (πΉβ(β‘πΉβ-ππ§)) = -ππ§) |
111 | 21, 93, 110 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (πΉβ(β‘πΉβ-ππ§)) = -ππ§) |
112 | | 0elunit 13315 |
. . . . . . . . . . . . . . . 16
β’ 0 β
(0[,]1) |
113 | | ax-1ne0 11054 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
0 |
114 | | neeq2 3006 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = 0 β (1 β π₯ β 1 β
0)) |
115 | 113, 114 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = 0 β 1 β π₯) |
116 | 115 | necomd 2998 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = 0 β π₯ β 1) |
117 | | ifnefalse 4497 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β 1 β if(π₯ = 1, +β, (π₯ / (1 β π₯))) = (π₯ / (1 β π₯))) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = 0 β if(π₯ = 1, +β, (π₯ / (1 β π₯))) = (π₯ / (1 β π₯))) |
119 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = 0 β π₯ = 0) |
120 | | oveq2 7358 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = 0 β (1 β π₯) = (1 β
0)) |
121 | | 1m0e1 12208 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1
β 0) = 1 |
122 | 120, 121 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = 0 β (1 β π₯) = 1) |
123 | 119, 122 | oveq12d 7368 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = 0 β (π₯ / (1 β π₯)) = (0 / 1)) |
124 | | ax-1cn 11043 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
β |
125 | 124, 113 | div0i 11823 |
. . . . . . . . . . . . . . . . . . 19
β’ (0 / 1) =
0 |
126 | 123, 125 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = 0 β (π₯ / (1 β π₯)) = 0) |
127 | 118, 126 | eqtrd 2778 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = 0 β if(π₯ = 1, +β, (π₯ / (1 β π₯))) = 0) |
128 | | c0ex 11083 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
V |
129 | 127, 19, 128 | fvmpt 6944 |
. . . . . . . . . . . . . . . 16
β’ (0 β
(0[,]1) β (πΉβ0)
= 0) |
130 | 112, 129 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (πΉβ0) = 0 |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (πΉβ0) =
0) |
132 | 111, 131 | breq12d 5117 |
. . . . . . . . . . . . 13
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β ((πΉβ(β‘πΉβ-ππ§)) β€ (πΉβ0) β -ππ§ β€ 0)) |
133 | 109, 132 | mtbird 325 |
. . . . . . . . . . . 12
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β Β¬ (πΉβ(β‘πΉβ-ππ§)) β€ (πΉβ0)) |
134 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
β’
((ordTopβ β€ ) βΎt (0[,]+β)) =
((ordTopβ β€ ) βΎt (0[,]+β)) |
135 | 19, 134 | iccpnfhmeo 24230 |
. . . . . . . . . . . . . . 15
β’ (πΉ Isom < , < ((0[,]1),
(0[,]+β)) β§ πΉ
β (IIHomeo((ordTopβ β€ ) βΎt
(0[,]+β)))) |
136 | 135 | simpli 485 |
. . . . . . . . . . . . . 14
β’ πΉ Isom < , < ((0[,]1),
(0[,]+β)) |
137 | | iccssxr 13276 |
. . . . . . . . . . . . . . 15
β’ (0[,]1)
β β* |
138 | 137, 8 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ ((0[,]1)
β β* β§ (0[,]+β) β
β*) |
139 | | leisorel 14287 |
. . . . . . . . . . . . . 14
β’ ((πΉ Isom < , < ((0[,]1),
(0[,]+β)) β§ ((0[,]1) β β* β§ (0[,]+β)
β β*) β§ ((β‘πΉβ-ππ§) β (0[,]1) β§ 0 β
(0[,]1))) β ((β‘πΉβ-ππ§) β€ 0 β (πΉβ(β‘πΉβ-ππ§)) β€ (πΉβ0))) |
140 | 136, 138,
139 | mp3an12 1452 |
. . . . . . . . . . . . 13
β’ (((β‘πΉβ-ππ§) β (0[,]1) β§ 0 β
(0[,]1)) β ((β‘πΉβ-ππ§) β€ 0 β (πΉβ(β‘πΉβ-ππ§)) β€ (πΉβ0))) |
141 | 95, 112, 140 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β ((β‘πΉβ-ππ§) β€ 0 β (πΉβ(β‘πΉβ-ππ§)) β€ (πΉβ0))) |
142 | 133, 141 | mtbird 325 |
. . . . . . . . . . 11
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β Β¬ (β‘πΉβ-ππ§) β€ 0) |
143 | 99 | le0neg1d 11660 |
. . . . . . . . . . 11
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β ((β‘πΉβ-ππ§) β€ 0 β 0 β€ -(β‘πΉβ-ππ§))) |
144 | 142, 143 | mtbid 324 |
. . . . . . . . . 10
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β Β¬ 0 β€ -(β‘πΉβ-ππ§)) |
145 | | unitssre 13345 |
. . . . . . . . . . . . . . . . 17
β’ (0[,]1)
β β |
146 | 145, 95 | sselid 3941 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (β‘πΉβ-ππ§) β
β) |
147 | 146 | recnd 11117 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (β‘πΉβ-ππ§) β
β) |
148 | 147 | negnegd 11437 |
. . . . . . . . . . . . . 14
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β --(β‘πΉβ-ππ§) = (β‘πΉβ-ππ§)) |
149 | 148 | fveq2d 6842 |
. . . . . . . . . . . . 13
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (πΉβ--(β‘πΉβ-ππ§)) = (πΉβ(β‘πΉβ-ππ§))) |
150 | 149, 111 | eqtrd 2778 |
. . . . . . . . . . . 12
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β (πΉβ--(β‘πΉβ-ππ§)) = -ππ§) |
151 | | xnegeq 13055 |
. . . . . . . . . . . 12
β’ ((πΉβ--(β‘πΉβ-ππ§)) = -ππ§ β
-π(πΉβ--(β‘πΉβ-ππ§)) =
-π-ππ§) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . 11
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β -π(πΉβ--(β‘πΉβ-ππ§)) =
-π-ππ§) |
153 | | xnegneg 13062 |
. . . . . . . . . . . 12
β’ (π§ β β*
β -π-ππ§ = π§) |
154 | 153 | adantr 482 |
. . . . . . . . . . 11
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β -π-ππ§ = π§) |
155 | 152, 154 | eqtr2d 2779 |
. . . . . . . . . 10
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β π§ =
-π(πΉβ--(β‘πΉβ-ππ§))) |
156 | | breq2 5108 |
. . . . . . . . . . . . 13
β’ (π¦ = -(β‘πΉβ-ππ§) β (0 β€ π¦ β 0 β€ -(β‘πΉβ-ππ§))) |
157 | 156 | notbid 318 |
. . . . . . . . . . . 12
β’ (π¦ = -(β‘πΉβ-ππ§) β (Β¬ 0 β€ π¦ β Β¬ 0 β€ -(β‘πΉβ-ππ§))) |
158 | | negeq 11327 |
. . . . . . . . . . . . . . 15
β’ (π¦ = -(β‘πΉβ-ππ§) β -π¦ = --(β‘πΉβ-ππ§)) |
159 | 158 | fveq2d 6842 |
. . . . . . . . . . . . . 14
β’ (π¦ = -(β‘πΉβ-ππ§) β (πΉβ-π¦) = (πΉβ--(β‘πΉβ-ππ§))) |
160 | | xnegeq 13055 |
. . . . . . . . . . . . . 14
β’ ((πΉβ-π¦) = (πΉβ--(β‘πΉβ-ππ§)) β
-π(πΉβ-π¦) = -π(πΉβ--(β‘πΉβ-ππ§))) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . 13
β’ (π¦ = -(β‘πΉβ-ππ§) β
-π(πΉβ-π¦) = -π(πΉβ--(β‘πΉβ-ππ§))) |
162 | 161 | eqeq2d 2749 |
. . . . . . . . . . . 12
β’ (π¦ = -(β‘πΉβ-ππ§) β (π§ = -π(πΉβ-π¦) β π§ = -π(πΉβ--(β‘πΉβ-ππ§)))) |
163 | 157, 162 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π¦ = -(β‘πΉβ-ππ§) β ((Β¬ 0 β€ π¦ β§ π§ = -π(πΉβ-π¦)) β (Β¬ 0 β€ -(β‘πΉβ-ππ§) β§ π§ = -π(πΉβ--(β‘πΉβ-ππ§))))) |
164 | 163 | rspcev 3580 |
. . . . . . . . . 10
β’ ((-(β‘πΉβ-ππ§) β (-1[,]1) β§ (Β¬ 0
β€ -(β‘πΉβ-ππ§) β§ π§ = -π(πΉβ--(β‘πΉβ-ππ§)))) β βπ¦ β (-1[,]1)(Β¬ 0 β€
π¦ β§ π§ = -π(πΉβ-π¦))) |
165 | 106, 144,
155, 164 | syl12anc 836 |
. . . . . . . . 9
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β βπ¦ β
(-1[,]1)(Β¬ 0 β€ π¦
β§ π§ =
-π(πΉβ-π¦))) |
166 | | iffalse 4494 |
. . . . . . . . . . . 12
β’ (Β¬ 0
β€ π¦ β if(0 β€
π¦, (πΉβπ¦), -π(πΉβ-π¦)) = -π(πΉβ-π¦)) |
167 | 166 | eqeq2d 2749 |
. . . . . . . . . . 11
β’ (Β¬ 0
β€ π¦ β (π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦)) β π§ = -π(πΉβ-π¦))) |
168 | 167 | biimpar 479 |
. . . . . . . . . 10
β’ ((Β¬ 0
β€ π¦ β§ π§ = -π(πΉβ-π¦)) β π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
169 | 168 | reximi 3086 |
. . . . . . . . 9
β’
(βπ¦ β
(-1[,]1)(Β¬ 0 β€ π¦
β§ π§ =
-π(πΉβ-π¦)) β βπ¦ β (-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
170 | 165, 169 | syl 17 |
. . . . . . . 8
β’ ((π§ β β*
β§ Β¬ 0 β€ π§)
β βπ¦ β
(-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
171 | 82, 170 | pm2.61dan 812 |
. . . . . . 7
β’ (π§ β β*
β βπ¦ β
(-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) |
172 | 50, 171 | mprgbir 3070 |
. . . . . 6
β’
β* β {π§ β£ βπ¦ β (-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))} |
173 | 7 | rnmpt 5907 |
. . . . . 6
β’ ran πΊ = {π§ β£ βπ¦ β (-1[,]1)π§ = if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))} |
174 | 172, 173 | sseqtrri 3980 |
. . . . 5
β’
β* β ran πΊ |
175 | 49, 174 | eqssi 3959 |
. . . 4
β’ ran πΊ =
β* |
176 | | dffo2 6756 |
. . . 4
β’ (πΊ:(-1[,]1)βontoββ* β (πΊ:(-1[,]1)βΆβ* β§
ran πΊ =
β*)) |
177 | 47, 175, 176 | mpbir2an 710 |
. . 3
β’ πΊ:(-1[,]1)βontoββ* |
178 | | breq1 5107 |
. . . . . . 7
β’ ((πΉβπ§) = if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§)) β ((πΉβπ§) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)) β if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§)) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)))) |
179 | | breq1 5107 |
. . . . . . 7
β’
(-π(πΉβ-π§) = if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§)) β (-π(πΉβ-π§) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)) β if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§)) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)))) |
180 | | simpl3 1194 |
. . . . . . . . 9
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β π§ < π€) |
181 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β π§ β (-1[,]1)) |
182 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β 0 β€ π§) |
183 | | breq2 5108 |
. . . . . . . . . . . . 13
β’ (π¦ = π§ β (0 β€ π¦ β 0 β€ π§)) |
184 | | eleq1w 2821 |
. . . . . . . . . . . . 13
β’ (π¦ = π§ β (π¦ β (0[,]1) β π§ β (0[,]1))) |
185 | 183, 184 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β ((0 β€ π¦ β π¦ β (0[,]1)) β (0 β€ π§ β π§ β (0[,]1)))) |
186 | 18 | ex 414 |
. . . . . . . . . . . 12
β’ (π¦ β (-1[,]1) β (0 β€
π¦ β π¦ β (0[,]1))) |
187 | 185, 186 | vtoclga 3533 |
. . . . . . . . . . 11
β’ (π§ β (-1[,]1) β (0 β€
π§ β π§ β (0[,]1))) |
188 | 181, 182,
187 | sylc 65 |
. . . . . . . . . 10
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β π§ β (0[,]1)) |
189 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β π€ β (-1[,]1)) |
190 | 29 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β 0 β β) |
191 | 98, 181 | sselid 3941 |
. . . . . . . . . . . 12
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β π§ β β) |
192 | 98, 189 | sselid 3941 |
. . . . . . . . . . . 12
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β π€ β β) |
193 | 191, 192,
180 | ltled 11237 |
. . . . . . . . . . . 12
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β π§ β€ π€) |
194 | 190, 191,
192, 182, 193 | letrd 11246 |
. . . . . . . . . . 11
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β 0 β€ π€) |
195 | | breq2 5108 |
. . . . . . . . . . . . 13
β’ (π¦ = π€ β (0 β€ π¦ β 0 β€ π€)) |
196 | | eleq1w 2821 |
. . . . . . . . . . . . 13
β’ (π¦ = π€ β (π¦ β (0[,]1) β π€ β (0[,]1))) |
197 | 195, 196 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π¦ = π€ β ((0 β€ π¦ β π¦ β (0[,]1)) β (0 β€ π€ β π€ β (0[,]1)))) |
198 | 197, 186 | vtoclga 3533 |
. . . . . . . . . . 11
β’ (π€ β (-1[,]1) β (0 β€
π€ β π€ β (0[,]1))) |
199 | 189, 194,
198 | sylc 65 |
. . . . . . . . . 10
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β π€ β (0[,]1)) |
200 | | isorel 7266 |
. . . . . . . . . . 11
β’ ((πΉ Isom < , < ((0[,]1),
(0[,]+β)) β§ (π§
β (0[,]1) β§ π€
β (0[,]1))) β (π§
< π€ β (πΉβπ§) < (πΉβπ€))) |
201 | 136, 200 | mpan 689 |
. . . . . . . . . 10
β’ ((π§ β (0[,]1) β§ π€ β (0[,]1)) β (π§ < π€ β (πΉβπ§) < (πΉβπ€))) |
202 | 188, 199,
201 | syl2anc 585 |
. . . . . . . . 9
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β (π§ < π€ β (πΉβπ§) < (πΉβπ€))) |
203 | 180, 202 | mpbid 231 |
. . . . . . . 8
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β (πΉβπ§) < (πΉβπ€)) |
204 | 194 | iftrued 4493 |
. . . . . . . 8
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)) = (πΉβπ€)) |
205 | 203, 204 | breqtrrd 5132 |
. . . . . . 7
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ 0 β€ π§) β (πΉβπ§) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€))) |
206 | | breq2 5108 |
. . . . . . . 8
β’ ((πΉβπ€) = if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)) β (-π(πΉβ-π§) < (πΉβπ€) β -π(πΉβ-π§) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)))) |
207 | | breq2 5108 |
. . . . . . . 8
β’
(-π(πΉβ-π€) = if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)) β (-π(πΉβ-π§) < -π(πΉβ-π€) β -π(πΉβ-π§) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)))) |
208 | | simpl1 1192 |
. . . . . . . . . . . . . 14
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β π§ β (-1[,]1)) |
209 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β Β¬ 0 β€ π§) |
210 | 183 | notbid 318 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π§ β (Β¬ 0 β€ π¦ β Β¬ 0 β€ π§)) |
211 | | negeq 11327 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π§ β -π¦ = -π§) |
212 | 211 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π§ β (-π¦ β (0[,]1) β -π§ β (0[,]1))) |
213 | 210, 212 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π§ β ((Β¬ 0 β€ π¦ β -π¦ β (0[,]1)) β (Β¬ 0 β€ π§ β -π§ β (0[,]1)))) |
214 | 41 | ex 414 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (-1[,]1) β (Β¬ 0
β€ π¦ β -π¦ β
(0[,]1))) |
215 | 213, 214 | vtoclga 3533 |
. . . . . . . . . . . . . 14
β’ (π§ β (-1[,]1) β (Β¬ 0
β€ π§ β -π§ β
(0[,]1))) |
216 | 208, 209,
215 | sylc 65 |
. . . . . . . . . . . . 13
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β -π§ β (0[,]1)) |
217 | 216 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β -π§ β (0[,]1)) |
218 | 23 | ffvelcdmi 7029 |
. . . . . . . . . . . 12
β’ (-π§ β (0[,]1) β (πΉβ-π§) β (0[,]+β)) |
219 | 217, 218 | syl 17 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (πΉβ-π§) β (0[,]+β)) |
220 | 8, 219 | sselid 3941 |
. . . . . . . . . 10
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (πΉβ-π§) β
β*) |
221 | 220 | xnegcld 13148 |
. . . . . . . . 9
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β -π(πΉβ-π§) β
β*) |
222 | 85 | a1i 11 |
. . . . . . . . 9
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β 0 β
β*) |
223 | | simpll2 1214 |
. . . . . . . . . . . 12
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β π€ β (-1[,]1)) |
224 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β 0 β€ π€) |
225 | 223, 224,
198 | sylc 65 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β π€ β (0[,]1)) |
226 | 23 | ffvelcdmi 7029 |
. . . . . . . . . . 11
β’ (π€ β (0[,]1) β (πΉβπ€) β (0[,]+β)) |
227 | 225, 226 | syl 17 |
. . . . . . . . . 10
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (πΉβπ€) β (0[,]+β)) |
228 | 8, 227 | sselid 3941 |
. . . . . . . . 9
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (πΉβπ€) β
β*) |
229 | 209 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β Β¬ 0 β€ π§) |
230 | | simpll1 1213 |
. . . . . . . . . . . . . . . 16
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β π§ β (-1[,]1)) |
231 | 98, 230 | sselid 3941 |
. . . . . . . . . . . . . . 15
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β π§ β β) |
232 | | ltnle 11168 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β β§ 0 β
β) β (π§ < 0
β Β¬ 0 β€ π§)) |
233 | 231, 29, 232 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (π§ < 0 β Β¬ 0 β€ π§)) |
234 | 229, 233 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β π§ < 0) |
235 | 231 | lt0neg1d 11658 |
. . . . . . . . . . . . 13
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (π§ < 0 β 0 < -π§)) |
236 | 234, 235 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β 0 < -π§) |
237 | | isorel 7266 |
. . . . . . . . . . . . . 14
β’ ((πΉ Isom < , < ((0[,]1),
(0[,]+β)) β§ (0 β (0[,]1) β§ -π§ β (0[,]1))) β (0 < -π§ β (πΉβ0) < (πΉβ-π§))) |
238 | 136, 237 | mpan 689 |
. . . . . . . . . . . . 13
β’ ((0
β (0[,]1) β§ -π§
β (0[,]1)) β (0 < -π§ β (πΉβ0) < (πΉβ-π§))) |
239 | 112, 217,
238 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (0 < -π§ β (πΉβ0) < (πΉβ-π§))) |
240 | 236, 239 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (πΉβ0) < (πΉβ-π§)) |
241 | 130, 240 | eqbrtrrid 5140 |
. . . . . . . . . 10
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β 0 < (πΉβ-π§)) |
242 | | xlt0neg2 13068 |
. . . . . . . . . . 11
β’ ((πΉβ-π§) β β* β (0 <
(πΉβ-π§) β
-π(πΉβ-π§) < 0)) |
243 | 220, 242 | syl 17 |
. . . . . . . . . 10
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β (0 < (πΉβ-π§) β -π(πΉβ-π§) < 0)) |
244 | 241, 243 | mpbid 231 |
. . . . . . . . 9
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β -π(πΉβ-π§) < 0) |
245 | | elxrge0 13303 |
. . . . . . . . . . 11
β’ ((πΉβπ€) β (0[,]+β) β ((πΉβπ€) β β* β§ 0 β€
(πΉβπ€))) |
246 | 245 | simprbi 498 |
. . . . . . . . . 10
β’ ((πΉβπ€) β (0[,]+β) β 0 β€ (πΉβπ€)) |
247 | 227, 246 | syl 17 |
. . . . . . . . 9
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β 0 β€ (πΉβπ€)) |
248 | 221, 222,
228, 244, 247 | xrltletrd 13009 |
. . . . . . . 8
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ 0 β€ π€) β -π(πΉβ-π§) < (πΉβπ€)) |
249 | | simpll3 1215 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β π§ < π€) |
250 | | simpll1 1213 |
. . . . . . . . . . . . 13
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β π§ β (-1[,]1)) |
251 | 98, 250 | sselid 3941 |
. . . . . . . . . . . 12
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β π§ β β) |
252 | | simpll2 1214 |
. . . . . . . . . . . . 13
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β π€ β (-1[,]1)) |
253 | 98, 252 | sselid 3941 |
. . . . . . . . . . . 12
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β π€ β β) |
254 | 251, 253 | ltnegd 11667 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β (π§ < π€ β -π€ < -π§)) |
255 | 249, 254 | mpbid 231 |
. . . . . . . . . 10
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β -π€ < -π§) |
256 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β Β¬ 0 β€ π€) |
257 | 195 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π¦ = π€ β (Β¬ 0 β€ π¦ β Β¬ 0 β€ π€)) |
258 | | negeq 11327 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π€ β -π¦ = -π€) |
259 | 258 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π¦ = π€ β (-π¦ β (0[,]1) β -π€ β (0[,]1))) |
260 | 257, 259 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π¦ = π€ β ((Β¬ 0 β€ π¦ β -π¦ β (0[,]1)) β (Β¬ 0 β€ π€ β -π€ β (0[,]1)))) |
261 | 260, 214 | vtoclga 3533 |
. . . . . . . . . . . 12
β’ (π€ β (-1[,]1) β (Β¬ 0
β€ π€ β -π€ β
(0[,]1))) |
262 | 252, 256,
261 | sylc 65 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β -π€ β (0[,]1)) |
263 | 216 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β -π§ β (0[,]1)) |
264 | | isorel 7266 |
. . . . . . . . . . . 12
β’ ((πΉ Isom < , < ((0[,]1),
(0[,]+β)) β§ (-π€
β (0[,]1) β§ -π§
β (0[,]1))) β (-π€
< -π§ β (πΉβ-π€) < (πΉβ-π§))) |
265 | 136, 264 | mpan 689 |
. . . . . . . . . . 11
β’ ((-π€ β (0[,]1) β§ -π§ β (0[,]1)) β (-π€ < -π§ β (πΉβ-π€) < (πΉβ-π§))) |
266 | 262, 263,
265 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β (-π€ < -π§ β (πΉβ-π€) < (πΉβ-π§))) |
267 | 255, 266 | mpbid 231 |
. . . . . . . . 9
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β (πΉβ-π€) < (πΉβ-π§)) |
268 | 23 | ffvelcdmi 7029 |
. . . . . . . . . . . 12
β’ (-π€ β (0[,]1) β (πΉβ-π€) β (0[,]+β)) |
269 | 262, 268 | syl 17 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β (πΉβ-π€) β (0[,]+β)) |
270 | 8, 269 | sselid 3941 |
. . . . . . . . . 10
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β (πΉβ-π€) β
β*) |
271 | 263, 218 | syl 17 |
. . . . . . . . . . 11
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β (πΉβ-π§) β (0[,]+β)) |
272 | 8, 271 | sselid 3941 |
. . . . . . . . . 10
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β (πΉβ-π§) β
β*) |
273 | | xltneg 13065 |
. . . . . . . . . 10
β’ (((πΉβ-π€) β β* β§ (πΉβ-π§) β β*) β ((πΉβ-π€) < (πΉβ-π§) β -π(πΉβ-π§) < -π(πΉβ-π€))) |
274 | 270, 272,
273 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β ((πΉβ-π€) < (πΉβ-π§) β -π(πΉβ-π§) < -π(πΉβ-π€))) |
275 | 267, 274 | mpbid 231 |
. . . . . . . 8
β’ ((((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β§ Β¬ 0 β€ π€) β -π(πΉβ-π§) < -π(πΉβ-π€)) |
276 | 206, 207,
248, 275 | ifbothda 4523 |
. . . . . . 7
β’ (((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β§ Β¬ 0 β€ π§) β -π(πΉβ-π§) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€))) |
277 | 178, 179,
205, 276 | ifbothda 4523 |
. . . . . 6
β’ ((π§ β (-1[,]1) β§ π€ β (-1[,]1) β§ π§ < π€) β if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§)) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€))) |
278 | 277 | 3expia 1122 |
. . . . 5
β’ ((π§ β (-1[,]1) β§ π€ β (-1[,]1)) β (π§ < π€ β if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§)) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)))) |
279 | | fveq2 6838 |
. . . . . . . 8
β’ (π¦ = π§ β (πΉβπ¦) = (πΉβπ§)) |
280 | 211 | fveq2d 6842 |
. . . . . . . . 9
β’ (π¦ = π§ β (πΉβ-π¦) = (πΉβ-π§)) |
281 | | xnegeq 13055 |
. . . . . . . . 9
β’ ((πΉβ-π¦) = (πΉβ-π§) β -π(πΉβ-π¦) = -π(πΉβ-π§)) |
282 | 280, 281 | syl 17 |
. . . . . . . 8
β’ (π¦ = π§ β -π(πΉβ-π¦) = -π(πΉβ-π§)) |
283 | 183, 279,
282 | ifbieq12d 4513 |
. . . . . . 7
β’ (π¦ = π§ β if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦)) = if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§))) |
284 | | fvex 6851 |
. . . . . . . 8
β’ (πΉβπ§) β V |
285 | | xnegex 13056 |
. . . . . . . 8
β’
-π(πΉβ-π§) β V |
286 | 284, 285 | ifex 4535 |
. . . . . . 7
β’ if(0 β€
π§, (πΉβπ§), -π(πΉβ-π§)) β V |
287 | 283, 7, 286 | fvmpt 6944 |
. . . . . 6
β’ (π§ β (-1[,]1) β (πΊβπ§) = if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§))) |
288 | | fveq2 6838 |
. . . . . . . 8
β’ (π¦ = π€ β (πΉβπ¦) = (πΉβπ€)) |
289 | 258 | fveq2d 6842 |
. . . . . . . . 9
β’ (π¦ = π€ β (πΉβ-π¦) = (πΉβ-π€)) |
290 | | xnegeq 13055 |
. . . . . . . . 9
β’ ((πΉβ-π¦) = (πΉβ-π€) β -π(πΉβ-π¦) = -π(πΉβ-π€)) |
291 | 289, 290 | syl 17 |
. . . . . . . 8
β’ (π¦ = π€ β -π(πΉβ-π¦) = -π(πΉβ-π€)) |
292 | 195, 288,
291 | ifbieq12d 4513 |
. . . . . . 7
β’ (π¦ = π€ β if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦)) = if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€))) |
293 | | fvex 6851 |
. . . . . . . 8
β’ (πΉβπ€) β V |
294 | | xnegex 13056 |
. . . . . . . 8
β’
-π(πΉβ-π€) β V |
295 | 293, 294 | ifex 4535 |
. . . . . . 7
β’ if(0 β€
π€, (πΉβπ€), -π(πΉβ-π€)) β V |
296 | 292, 7, 295 | fvmpt 6944 |
. . . . . 6
β’ (π€ β (-1[,]1) β (πΊβπ€) = if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€))) |
297 | 287, 296 | breqan12d 5120 |
. . . . 5
β’ ((π§ β (-1[,]1) β§ π€ β (-1[,]1)) β ((πΊβπ§) < (πΊβπ€) β if(0 β€ π§, (πΉβπ§), -π(πΉβ-π§)) < if(0 β€ π€, (πΉβπ€), -π(πΉβ-π€)))) |
298 | 278, 297 | sylibrd 259 |
. . . 4
β’ ((π§ β (-1[,]1) β§ π€ β (-1[,]1)) β (π§ < π€ β (πΊβπ§) < (πΊβπ€))) |
299 | 298 | rgen2 3193 |
. . 3
β’
βπ§ β
(-1[,]1)βπ€ β
(-1[,]1)(π§ < π€ β (πΊβπ§) < (πΊβπ€)) |
300 | | soisoi 7268 |
. . 3
β’ ((( <
Or (-1[,]1) β§ < Po β*) β§ (πΊ:(-1[,]1)βontoββ* β§ βπ§ β (-1[,]1)βπ€ β (-1[,]1)(π§ < π€ β (πΊβπ§) < (πΊβπ€)))) β πΊ Isom < , < ((-1[,]1),
β*)) |
301 | 4, 6, 177, 299, 300 | mp4an 692 |
. 2
β’ πΊ Isom < , < ((-1[,]1),
β*) |
302 | | letsr 18417 |
. . . . . 6
β’ β€
β TosetRel |
303 | 302 | elexi 3463 |
. . . . 5
β’ β€
β V |
304 | 303 | inex1 5273 |
. . . 4
β’ ( β€
β© ((-1[,]1) Γ (-1[,]1))) β V |
305 | | ssid 3965 |
. . . . . . 7
β’
β* β β* |
306 | | leiso 14286 |
. . . . . . 7
β’
(((-1[,]1) β β* β§ β* β
β*) β (πΊ Isom < , < ((-1[,]1),
β*) β πΊ Isom β€ , β€ ((-1[,]1),
β*))) |
307 | 1, 305, 306 | mp2an 691 |
. . . . . 6
β’ (πΊ Isom < , < ((-1[,]1),
β*) β πΊ Isom β€ , β€ ((-1[,]1),
β*)) |
308 | 301, 307 | mpbi 229 |
. . . . 5
β’ πΊ Isom β€ , β€ ((-1[,]1),
β*) |
309 | | isores1 7274 |
. . . . 5
β’ (πΊ Isom β€ , β€ ((-1[,]1),
β*) β πΊ Isom ( β€ β© ((-1[,]1) Γ
(-1[,]1))), β€ ((-1[,]1), β*)) |
310 | 308, 309 | mpbi 229 |
. . . 4
β’ πΊ Isom ( β€ β© ((-1[,]1)
Γ (-1[,]1))), β€ ((-1[,]1), β*) |
311 | | tsrps 18411 |
. . . . . . . 8
β’ ( β€
β TosetRel β β€ β PosetRel) |
312 | 302, 311 | ax-mp 5 |
. . . . . . 7
β’ β€
β PosetRel |
313 | | ledm 18414 |
. . . . . . . 8
β’
β* = dom β€ |
314 | 313 | psssdm 18406 |
. . . . . . 7
β’ (( β€
β PosetRel β§ (-1[,]1) β β*) β dom ( β€
β© ((-1[,]1) Γ (-1[,]1))) = (-1[,]1)) |
315 | 312, 1, 314 | mp2an 691 |
. . . . . 6
β’ dom (
β€ β© ((-1[,]1) Γ (-1[,]1))) = (-1[,]1) |
316 | 315 | eqcomi 2747 |
. . . . 5
β’ (-1[,]1)
= dom ( β€ β© ((-1[,]1) Γ (-1[,]1))) |
317 | 316, 313 | ordthmeo 23075 |
. . . 4
β’ ((( β€
β© ((-1[,]1) Γ (-1[,]1))) β V β§ β€ β TosetRel β§
πΊ Isom ( β€ β©
((-1[,]1) Γ (-1[,]1))), β€ ((-1[,]1), β*)) β
πΊ β ((ordTopβ(
β€ β© ((-1[,]1) Γ (-1[,]1))))Homeo(ordTopβ β€
))) |
318 | 304, 302,
310, 317 | mp3an 1462 |
. . 3
β’ πΊ β ((ordTopβ( β€
β© ((-1[,]1) Γ (-1[,]1))))Homeo(ordTopβ β€ )) |
319 | | xrhmeo.j |
. . . . . . 7
β’ π½ =
(TopOpenββfld) |
320 | | eqid 2738 |
. . . . . . 7
β’
(ordTopβ β€ ) = (ordTopβ β€ ) |
321 | 319, 320 | xrrest2 24093 |
. . . . . 6
β’ ((-1[,]1)
β β β (π½
βΎt (-1[,]1)) = ((ordTopβ β€ ) βΎt
(-1[,]1))) |
322 | 98, 321 | ax-mp 5 |
. . . . 5
β’ (π½ βΎt (-1[,]1)) =
((ordTopβ β€ ) βΎt (-1[,]1)) |
323 | | ordtresticc 22496 |
. . . . 5
β’
((ordTopβ β€ ) βΎt (-1[,]1)) = (ordTopβ(
β€ β© ((-1[,]1) Γ (-1[,]1)))) |
324 | 322, 323 | eqtri 2766 |
. . . 4
β’ (π½ βΎt (-1[,]1)) =
(ordTopβ( β€ β© ((-1[,]1) Γ (-1[,]1)))) |
325 | 324 | oveq1i 7360 |
. . 3
β’ ((π½ βΎt
(-1[,]1))Homeo(ordTopβ β€ )) = ((ordTopβ( β€ β© ((-1[,]1)
Γ (-1[,]1))))Homeo(ordTopβ β€ )) |
326 | 318, 325 | eleqtrri 2838 |
. 2
β’ πΊ β ((π½ βΎt
(-1[,]1))Homeo(ordTopβ β€ )) |
327 | 301, 326 | pm3.2i 472 |
1
β’ (πΊ Isom < , < ((-1[,]1),
β*) β§ πΊ β ((π½ βΎt
(-1[,]1))Homeo(ordTopβ β€ ))) |