Metamath Proof Explorer

Theorem cnre2csqlem

Description: Lemma for cnre2csqima . (Contributed by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Hypotheses cnre2csqlem.1 
|- ( G |` ( RR X. RR ) ) = ( H o. F )
cnre2csqlem.2 
|- F Fn ( RR X. RR )
cnre2csqlem.3 
|- G Fn _V
cnre2csqlem.4 
|- ( x e. ( RR X. RR ) -> ( G ` x ) e. RR )
cnre2csqlem.5 
|- ( ( x e. ran F /\ y e. ran F ) -> ( H ` ( x - y ) ) = ( ( H ` x ) - ( H ` y ) ) )
Assertion cnre2csqlem 
|- ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( `' ( G |` ( RR X. RR ) ) " ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) -> ( abs ` ( H ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D ) )

Proof

Step Hyp Ref Expression
1 cnre2csqlem.1 
 |-  ( G |` ( RR X. RR ) ) = ( H o. F )
2 cnre2csqlem.2 
 |-  F Fn ( RR X. RR )
3 cnre2csqlem.3 
 |-  G Fn _V
4 cnre2csqlem.4 
 |-  ( x e. ( RR X. RR ) -> ( G ` x ) e. RR )
5 cnre2csqlem.5 
 |-  ( ( x e. ran F /\ y e. ran F ) -> ( H ` ( x - y ) ) = ( ( H ` x ) - ( H ` y ) ) )
6 ssv 
 |-  ( RR X. RR ) C_ _V
7 fnssres 
 |-  ( ( G Fn _V /\ ( RR X. RR ) C_ _V ) -> ( G |` ( RR X. RR ) ) Fn ( RR X. RR ) )
8 3 6 7 mp2an 
 |-  ( G |` ( RR X. RR ) ) Fn ( RR X. RR )
9 elpreima 
 |-  ( ( G |` ( RR X. RR ) ) Fn ( RR X. RR ) -> ( Y e. ( `' ( G |` ( RR X. RR ) ) " ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) <-> ( Y e. ( RR X. RR ) /\ ( ( G |` ( RR X. RR ) ) ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) ) )
10 8 9 mp1i 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( `' ( G |` ( RR X. RR ) ) " ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) <-> ( Y e. ( RR X. RR ) /\ ( ( G |` ( RR X. RR ) ) ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) ) )
11 10 simplbda 
 |-  ( ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) /\ Y e. ( `' ( G |` ( RR X. RR ) ) " ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) ) -> ( ( G |` ( RR X. RR ) ) ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) )
12 11 ex 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( `' ( G |` ( RR X. RR ) ) " ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) -> ( ( G |` ( RR X. RR ) ) ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) )
13 simp2 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> Y e. ( RR X. RR ) )
14 fvres 
 |-  ( Y e. ( RR X. RR ) -> ( ( G |` ( RR X. RR ) ) ` Y ) = ( G ` Y ) )
15 13 14 syl 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G |` ( RR X. RR ) ) ` Y ) = ( G ` Y ) )
16 15 eleq1d 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( ( G |` ( RR X. RR ) ) ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) <-> ( G ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) )
17 simp1 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> X e. ( RR X. RR ) )
18 fveq2 
 |-  ( x = X -> ( G ` x ) = ( G ` X ) )
19 18 eleq1d 
 |-  ( x = X -> ( ( G ` x ) e. RR <-> ( G ` X ) e. RR ) )
20 19 4 vtoclga 
 |-  ( X e. ( RR X. RR ) -> ( G ` X ) e. RR )
21 17 20 syl 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( G ` X ) e. RR )
22 simp3 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> D e. RR+ )
23 22 rpred 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> D e. RR )
24 21 23 resubcld 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G ` X ) - D ) e. RR )
25 24 rexrd 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G ` X ) - D ) e. RR* )
26 21 23 readdcld 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G ` X ) + D ) e. RR )
27 26 rexrd 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G ` X ) + D ) e. RR* )
28 elioo2 
 |-  ( ( ( ( G ` X ) - D ) e. RR* /\ ( ( G ` X ) + D ) e. RR* ) -> ( ( G ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) <-> ( ( G ` Y ) e. RR /\ ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) ) )
29 25 27 28 syl2anc 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) <-> ( ( G ` Y ) e. RR /\ ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) ) )
30 29 biimpa 
 |-  ( ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) /\ ( G ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) -> ( ( G ` Y ) e. RR /\ ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) )
31 30 simp2d 
 |-  ( ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) /\ ( G ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) -> ( ( G ` X ) - D ) < ( G ` Y ) )
32 30 simp3d 
 |-  ( ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) /\ ( G ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) -> ( G ` Y ) < ( ( G ` X ) + D ) )
33 31 32 jca 
 |-  ( ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) /\ ( G ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) -> ( ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) )
34 33 ex 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) -> ( ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) ) )
35 16 34 sylbid 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( ( G |` ( RR X. RR ) ) ` Y ) e. ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) -> ( ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) ) )
36 fveq2 
 |-  ( x = Y -> ( G ` x ) = ( G ` Y ) )
37 36 eleq1d 
 |-  ( x = Y -> ( ( G ` x ) e. RR <-> ( G ` Y ) e. RR ) )
38 37 4 vtoclga 
 |-  ( Y e. ( RR X. RR ) -> ( G ` Y ) e. RR )
39 13 38 syl 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( G ` Y ) e. RR )
40 absdiflt 
 |-  ( ( ( G ` Y ) e. RR /\ ( G ` X ) e. RR /\ D e. RR ) -> ( ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) < D <-> ( ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) ) )
41 40 biimprd 
 |-  ( ( ( G ` Y ) e. RR /\ ( G ` X ) e. RR /\ D e. RR ) -> ( ( ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) < D ) )
42 39 21 23 41 syl3anc 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( ( ( G ` X ) - D ) < ( G ` Y ) /\ ( G ` Y ) < ( ( G ` X ) + D ) ) -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) < D ) )
43 12 35 42 3syld 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( `' ( G |` ( RR X. RR ) ) " ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) < D ) )
44 fnfvelrn 
 |-  ( ( F Fn ( RR X. RR ) /\ Y e. ( RR X. RR ) ) -> ( F ` Y ) e. ran F )
45 2 13 44 sylancr 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( F ` Y ) e. ran F )
46 fnfvelrn 
 |-  ( ( F Fn ( RR X. RR ) /\ X e. ( RR X. RR ) ) -> ( F ` X ) e. ran F )
47 2 17 46 sylancr 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( F ` X ) e. ran F )
48 fvoveq1 
 |-  ( x = ( F ` Y ) -> ( H ` ( x - y ) ) = ( H ` ( ( F ` Y ) - y ) ) )
49 fveq2 
 |-  ( x = ( F ` Y ) -> ( H ` x ) = ( H ` ( F ` Y ) ) )
50 49 oveq1d 
 |-  ( x = ( F ` Y ) -> ( ( H ` x ) - ( H ` y ) ) = ( ( H ` ( F ` Y ) ) - ( H ` y ) ) )
51 48 50 eqeq12d 
 |-  ( x = ( F ` Y ) -> ( ( H ` ( x - y ) ) = ( ( H ` x ) - ( H ` y ) ) <-> ( H ` ( ( F ` Y ) - y ) ) = ( ( H ` ( F ` Y ) ) - ( H ` y ) ) ) )
52 oveq2 
 |-  ( y = ( F ` X ) -> ( ( F ` Y ) - y ) = ( ( F ` Y ) - ( F ` X ) ) )
53 52 fveq2d 
 |-  ( y = ( F ` X ) -> ( H ` ( ( F ` Y ) - y ) ) = ( H ` ( ( F ` Y ) - ( F ` X ) ) ) )
54 fveq2 
 |-  ( y = ( F ` X ) -> ( H ` y ) = ( H ` ( F ` X ) ) )
55 54 oveq2d 
 |-  ( y = ( F ` X ) -> ( ( H ` ( F ` Y ) ) - ( H ` y ) ) = ( ( H ` ( F ` Y ) ) - ( H ` ( F ` X ) ) ) )
56 53 55 eqeq12d 
 |-  ( y = ( F ` X ) -> ( ( H ` ( ( F ` Y ) - y ) ) = ( ( H ` ( F ` Y ) ) - ( H ` y ) ) <-> ( H ` ( ( F ` Y ) - ( F ` X ) ) ) = ( ( H ` ( F ` Y ) ) - ( H ` ( F ` X ) ) ) ) )
57 51 56 5 vtocl2ga 
 |-  ( ( ( F ` Y ) e. ran F /\ ( F ` X ) e. ran F ) -> ( H ` ( ( F ` Y ) - ( F ` X ) ) ) = ( ( H ` ( F ` Y ) ) - ( H ` ( F ` X ) ) ) )
58 45 47 57 syl2anc 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( H ` ( ( F ` Y ) - ( F ` X ) ) ) = ( ( H ` ( F ` Y ) ) - ( H ` ( F ` X ) ) ) )
59 1 fveq1i 
 |-  ( ( G |` ( RR X. RR ) ) ` Y ) = ( ( H o. F ) ` Y )
60 fvco2 
 |-  ( ( F Fn ( RR X. RR ) /\ Y e. ( RR X. RR ) ) -> ( ( H o. F ) ` Y ) = ( H ` ( F ` Y ) ) )
61 2 13 60 sylancr 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( H o. F ) ` Y ) = ( H ` ( F ` Y ) ) )
62 59 15 61 3eqtr3a 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( G ` Y ) = ( H ` ( F ` Y ) ) )
63 1 fveq1i 
 |-  ( ( G |` ( RR X. RR ) ) ` X ) = ( ( H o. F ) ` X )
64 fvres 
 |-  ( X e. ( RR X. RR ) -> ( ( G |` ( RR X. RR ) ) ` X ) = ( G ` X ) )
65 17 64 syl 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G |` ( RR X. RR ) ) ` X ) = ( G ` X ) )
66 fvco2 
 |-  ( ( F Fn ( RR X. RR ) /\ X e. ( RR X. RR ) ) -> ( ( H o. F ) ` X ) = ( H ` ( F ` X ) ) )
67 2 17 66 sylancr 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( H o. F ) ` X ) = ( H ` ( F ` X ) ) )
68 63 65 67 3eqtr3a 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( G ` X ) = ( H ` ( F ` X ) ) )
69 62 68 oveq12d 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( G ` Y ) - ( G ` X ) ) = ( ( H ` ( F ` Y ) ) - ( H ` ( F ` X ) ) ) )
70 58 69 eqtr4d 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( H ` ( ( F ` Y ) - ( F ` X ) ) ) = ( ( G ` Y ) - ( G ` X ) ) )
71 70 fveq2d 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( abs ` ( H ` ( ( F ` Y ) - ( F ` X ) ) ) ) = ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) )
72 71 breq1d 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( abs ` ( H ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D <-> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) < D ) )
73 43 72 sylibrd 
 |-  ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( `' ( G |` ( RR X. RR ) ) " ( ( ( G ` X ) - D ) (,) ( ( G ` X ) + D ) ) ) -> ( abs ` ( H ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D ) )