This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem icchmeoOLD

Description: Obsolete version of icchmeo as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Sep-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses icchmeoOLD.j 
|- J = ( TopOpen ` CCfld )
icchmeoOLD.f 
|- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
Assertion icchmeoOLD 
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Homeo ( J |`t ( A [,] B ) ) ) )

Proof

Step Hyp Ref Expression
1 icchmeoOLD.j 
 |-  J = ( TopOpen ` CCfld )
2 icchmeoOLD.f 
 |-  F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
3 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
4 3 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
5 1 dfii3 
 |-  II = ( J |`t ( 0 [,] 1 ) )
6 5 oveq2i 
 |-  ( II Cn II ) = ( II Cn ( J |`t ( 0 [,] 1 ) ) )
7 1 cnfldtop 
 |-  J e. Top
8 cnrest2r 
 |-  ( J e. Top -> ( II Cn ( J |`t ( 0 [,] 1 ) ) ) C_ ( II Cn J ) )
9 7 8 ax-mp 
 |-  ( II Cn ( J |`t ( 0 [,] 1 ) ) ) C_ ( II Cn J )
10 6 9 eqsstri 
 |-  ( II Cn II ) C_ ( II Cn J )
11 4 cnmptid 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn II ) )
12 10 11 sselid 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn J ) )
13 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
14 13 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> J e. ( TopOn ` CC ) )
15 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. RR )
16 15 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. CC )
17 4 14 16 cnmptc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> B ) e. ( II Cn J ) )
18 1 mulcn 
 |-  x. e. ( ( J tX J ) Cn J )
19 18 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> x. e. ( ( J tX J ) Cn J ) )
20 4 12 17 19 cnmpt12f 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( x x. B ) ) e. ( II Cn J ) )
21 1cnd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> 1 e. CC )
22 4 14 21 cnmptc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> 1 ) e. ( II Cn J ) )
23 1 subcn 
 |-  - e. ( ( J tX J ) Cn J )
24 23 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> - e. ( ( J tX J ) Cn J ) )
25 4 22 12 24 cnmpt12f 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn J ) )
26 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. RR )
27 26 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. CC )
28 4 14 27 cnmptc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> A ) e. ( II Cn J ) )
29 4 25 28 19 cnmpt12f 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) x. A ) ) e. ( II Cn J ) )
30 1 addcn 
 |-  + e. ( ( J tX J ) Cn J )
31 30 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> + e. ( ( J tX J ) Cn J ) )
32 4 20 29 31 cnmpt12f 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) e. ( II Cn J ) )
33 2 32 eqeltrid 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Cn J ) )
34 2 iccf1o 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) /\ `' F = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) ) )
35 34 simpld 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) )
36 f1of 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) -> F : ( 0 [,] 1 ) --> ( A [,] B ) )
37 frn 
 |-  ( F : ( 0 [,] 1 ) --> ( A [,] B ) -> ran F C_ ( A [,] B ) )
38 35 36 37 3syl 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ran F C_ ( A [,] B ) )
39 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
40 39 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A [,] B ) C_ RR )
41 ax-resscn 
 |-  RR C_ CC
42 40 41 sstrdi 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A [,] B ) C_ CC )
43 cnrest2 
 |-  ( ( J e. ( TopOn ` CC ) /\ ran F C_ ( A [,] B ) /\ ( A [,] B ) C_ CC ) -> ( F e. ( II Cn J ) <-> F e. ( II Cn ( J |`t ( A [,] B ) ) ) ) )
44 13 38 42 43 mp3an2i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( F e. ( II Cn J ) <-> F e. ( II Cn ( J |`t ( A [,] B ) ) ) ) )
45 33 44 mpbid 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Cn ( J |`t ( A [,] B ) ) ) )
46 34 simprd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) )
47 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ ( A [,] B ) C_ CC ) -> ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) )
48 13 42 47 sylancr 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) )
49 cnrest2r 
 |-  ( J e. Top -> ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) C_ ( ( J |`t ( A [,] B ) ) Cn J ) )
50 7 49 ax-mp 
 |-  ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) C_ ( ( J |`t ( A [,] B ) ) Cn J )
51 48 cnmptid 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> y ) e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) )
52 50 51 sselid 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> y ) e. ( ( J |`t ( A [,] B ) ) Cn J ) )
53 48 14 27 cnmptc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> A ) e. ( ( J |`t ( A [,] B ) ) Cn J ) )
54 48 52 53 24 cnmpt12f 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> ( y - A ) ) e. ( ( J |`t ( A [,] B ) ) Cn J ) )
55 difrp 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )
56 55 biimp3a 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. RR+ )
57 56 rpcnd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. CC )
58 56 rpne0d 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) =/= 0 )
59 1 divccn 
 |-  ( ( ( B - A ) e. CC /\ ( B - A ) =/= 0 ) -> ( x e. CC |-> ( x / ( B - A ) ) ) e. ( J Cn J ) )
60 57 58 59 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. CC |-> ( x / ( B - A ) ) ) e. ( J Cn J ) )
61 oveq1 
 |-  ( x = ( y - A ) -> ( x / ( B - A ) ) = ( ( y - A ) / ( B - A ) ) )
62 48 54 14 60 61 cnmpt11 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) e. ( ( J |`t ( A [,] B ) ) Cn J ) )
63 46 62 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) )
64 dfdm4 
 |-  dom F = ran `' F
65 64 eqimss2i 
 |-  ran `' F C_ dom F
66 f1odm 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) -> dom F = ( 0 [,] 1 ) )
67 35 66 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> dom F = ( 0 [,] 1 ) )
68 65 67 sseqtrid 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ran `' F C_ ( 0 [,] 1 ) )
69 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
70 69 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) C_ RR )
71 70 41 sstrdi 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) C_ CC )
72 cnrest2 
 |-  ( ( J e. ( TopOn ` CC ) /\ ran `' F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ CC ) -> ( `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) <-> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) ) )
73 13 68 71 72 mp3an2i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) <-> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) ) )
74 63 73 mpbid 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) )
75 5 oveq2i 
 |-  ( ( J |`t ( A [,] B ) ) Cn II ) = ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) )
76 74 75 eleqtrrdi 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn II ) )
77 ishmeo 
 |-  ( F e. ( II Homeo ( J |`t ( A [,] B ) ) ) <-> ( F e. ( II Cn ( J |`t ( A [,] B ) ) ) /\ `' F e. ( ( J |`t ( A [,] B ) ) Cn II ) ) )
78 45 76 77 sylanbrc 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Homeo ( J |`t ( A [,] B ) ) ) )