Metamath Proof Explorer

Theorem cncfperiod

Description: A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfperiod.a 
|- ( ph -> A C_ CC )
cncfperiod.t 
|- ( ph -> T e. RR )
cncfperiod.b 
|- B = { x e. CC | E. y e. A x = ( y + T ) }
cncfperiod.f 
|- ( ph -> F : dom F --> CC )
cncfperiod.cssdmf 
|- ( ph -> B C_ dom F )
cncfperiod.fper 
|- ( ( ph /\ x e. A ) -> ( F ` ( x + T ) ) = ( F ` x ) )
cncfperiod.fcn 
|- ( ph -> ( F |` A ) e. ( A -cn-> CC ) )
Assertion cncfperiod 
|- ( ph -> ( F |` B ) e. ( B -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 cncfperiod.a 
 |-  ( ph -> A C_ CC )
2 cncfperiod.t 
 |-  ( ph -> T e. RR )
3 cncfperiod.b 
 |-  B = { x e. CC | E. y e. A x = ( y + T ) }
4 cncfperiod.f 
 |-  ( ph -> F : dom F --> CC )
5 cncfperiod.cssdmf 
 |-  ( ph -> B C_ dom F )
6 cncfperiod.fper 
 |-  ( ( ph /\ x e. A ) -> ( F ` ( x + T ) ) = ( F ` x ) )
7 cncfperiod.fcn 
 |-  ( ph -> ( F |` A ) e. ( A -cn-> CC ) )
8 4 5 fssresd 
 |-  ( ph -> ( F |` B ) : B --> CC )
9 fvoveq1 
 |-  ( a = ( x - T ) -> ( abs ` ( a - b ) ) = ( abs ` ( ( x - T ) - b ) ) )
10 9 breq1d 
 |-  ( a = ( x - T ) -> ( ( abs ` ( a - b ) ) < z <-> ( abs ` ( ( x - T ) - b ) ) < z ) )
11 10 imbrov2fvoveq 
 |-  ( a = ( x - T ) -> ( ( ( abs ` ( a - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` a ) - ( ( F |` A ) ` b ) ) ) < w ) <-> ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) )
12 11 rexralbidv 
 |-  ( a = ( x - T ) -> ( E. z e. RR+ A. b e. A ( ( abs ` ( a - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` a ) - ( ( F |` A ) ` b ) ) ) < w ) <-> E. z e. RR+ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) )
13 12 ralbidv 
 |-  ( a = ( x - T ) -> ( A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( a - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` a ) - ( ( F |` A ) ` b ) ) ) < w ) <-> A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) )
14 7 adantr 
 |-  ( ( ph /\ x e. B ) -> ( F |` A ) e. ( A -cn-> CC ) )
15 1 adantr 
 |-  ( ( ph /\ x e. B ) -> A C_ CC )
16 ssidd 
 |-  ( ( ph /\ x e. B ) -> CC C_ CC )
17 elcncf 
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( ( F |` A ) e. ( A -cn-> CC ) <-> ( ( F |` A ) : A --> CC /\ A. a e. A A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( a - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` a ) - ( ( F |` A ) ` b ) ) ) < w ) ) ) )
18 15 16 17 syl2anc 
 |-  ( ( ph /\ x e. B ) -> ( ( F |` A ) e. ( A -cn-> CC ) <-> ( ( F |` A ) : A --> CC /\ A. a e. A A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( a - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` a ) - ( ( F |` A ) ` b ) ) ) < w ) ) ) )
19 14 18 mpbid 
 |-  ( ( ph /\ x e. B ) -> ( ( F |` A ) : A --> CC /\ A. a e. A A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( a - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` a ) - ( ( F |` A ) ` b ) ) ) < w ) ) )
20 19 simprd 
 |-  ( ( ph /\ x e. B ) -> A. a e. A A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( a - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` a ) - ( ( F |` A ) ` b ) ) ) < w ) )
21 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
22 21 3 eleqtrdi 
 |-  ( ( ph /\ x e. B ) -> x e. { x e. CC | E. y e. A x = ( y + T ) } )
23 rabid 
 |-  ( x e. { x e. CC | E. y e. A x = ( y + T ) } <-> ( x e. CC /\ E. y e. A x = ( y + T ) ) )
24 22 23 sylib 
 |-  ( ( ph /\ x e. B ) -> ( x e. CC /\ E. y e. A x = ( y + T ) ) )
25 24 simprd 
 |-  ( ( ph /\ x e. B ) -> E. y e. A x = ( y + T ) )
26 oveq1 
 |-  ( x = ( y + T ) -> ( x - T ) = ( ( y + T ) - T ) )
27 26 3ad2ant3 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ x = ( y + T ) ) -> ( x - T ) = ( ( y + T ) - T ) )
28 1 sselda 
 |-  ( ( ph /\ y e. A ) -> y e. CC )
29 2 recnd 
 |-  ( ph -> T e. CC )
30 29 adantr 
 |-  ( ( ph /\ y e. A ) -> T e. CC )
31 28 30 pncand 
 |-  ( ( ph /\ y e. A ) -> ( ( y + T ) - T ) = y )
32 31 adantlr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A ) -> ( ( y + T ) - T ) = y )
33 32 3adant3 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ x = ( y + T ) ) -> ( ( y + T ) - T ) = y )
34 27 33 eqtrd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ x = ( y + T ) ) -> ( x - T ) = y )
35 simp2 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ x = ( y + T ) ) -> y e. A )
36 34 35 eqeltrd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ x = ( y + T ) ) -> ( x - T ) e. A )
37 36 rexlimdv3a 
 |-  ( ( ph /\ x e. B ) -> ( E. y e. A x = ( y + T ) -> ( x - T ) e. A ) )
38 25 37 mpd 
 |-  ( ( ph /\ x e. B ) -> ( x - T ) e. A )
39 13 20 38 rspcdva 
 |-  ( ( ph /\ x e. B ) -> A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) )
40 39 adantrr 
 |-  ( ( ph /\ ( x e. B /\ w e. RR+ ) ) -> A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) )
41 simprr 
 |-  ( ( ph /\ ( x e. B /\ w e. RR+ ) ) -> w e. RR+ )
42 rspa 
 |-  ( ( A. w e. RR+ E. z e. RR+ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) /\ w e. RR+ ) -> E. z e. RR+ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) )
43 40 41 42 syl2anc 
 |-  ( ( ph /\ ( x e. B /\ w e. RR+ ) ) -> E. z e. RR+ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) )
44 simpl1l 
 |-  ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) -> ph )
45 44 adantr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ph )
46 simp1rl 
 |-  ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) -> x e. B )
47 46 adantr 
 |-  ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) -> x e. B )
48 47 adantr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> x e. B )
49 simplr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> v e. B )
50 fvres 
 |-  ( x e. B -> ( ( F |` B ) ` x ) = ( F ` x ) )
51 50 adantl 
 |-  ( ( ph /\ x e. B ) -> ( ( F |` B ) ` x ) = ( F ` x ) )
52 3 ssrab3 
 |-  B C_ CC
53 52 sseli 
 |-  ( x e. B -> x e. CC )
54 53 adantl 
 |-  ( ( ph /\ x e. B ) -> x e. CC )
55 29 adantr 
 |-  ( ( ph /\ x e. B ) -> T e. CC )
56 54 55 npcand 
 |-  ( ( ph /\ x e. B ) -> ( ( x - T ) + T ) = x )
57 56 eqcomd 
 |-  ( ( ph /\ x e. B ) -> x = ( ( x - T ) + T ) )
58 57 fveq2d 
 |-  ( ( ph /\ x e. B ) -> ( F ` x ) = ( F ` ( ( x - T ) + T ) ) )
59 simpl 
 |-  ( ( ph /\ x e. B ) -> ph )
60 59 38 jca 
 |-  ( ( ph /\ x e. B ) -> ( ph /\ ( x - T ) e. A ) )
61 eleq1 
 |-  ( y = ( x - T ) -> ( y e. A <-> ( x - T ) e. A ) )
62 61 anbi2d 
 |-  ( y = ( x - T ) -> ( ( ph /\ y e. A ) <-> ( ph /\ ( x - T ) e. A ) ) )
63 fvoveq1 
 |-  ( y = ( x - T ) -> ( F ` ( y + T ) ) = ( F ` ( ( x - T ) + T ) ) )
64 fveq2 
 |-  ( y = ( x - T ) -> ( F ` y ) = ( F ` ( x - T ) ) )
65 63 64 eqeq12d 
 |-  ( y = ( x - T ) -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
66 62 65 imbi12d 
 |-  ( y = ( x - T ) -> ( ( ( ph /\ y e. A ) -> ( F ` ( y + T ) ) = ( F ` y ) ) <-> ( ( ph /\ ( x - T ) e. A ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) ) )
67 eleq1 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
68 67 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. A ) <-> ( ph /\ y e. A ) ) )
69 fvoveq1 
 |-  ( x = y -> ( F ` ( x + T ) ) = ( F ` ( y + T ) ) )
70 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
71 69 70 eqeq12d 
 |-  ( x = y -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( y + T ) ) = ( F ` y ) ) )
72 68 71 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ y e. A ) -> ( F ` ( y + T ) ) = ( F ` y ) ) ) )
73 72 6 chvarvv 
 |-  ( ( ph /\ y e. A ) -> ( F ` ( y + T ) ) = ( F ` y ) )
74 66 73 vtoclg 
 |-  ( ( x - T ) e. A -> ( ( ph /\ ( x - T ) e. A ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
75 38 60 74 sylc 
 |-  ( ( ph /\ x e. B ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) )
76 38 fvresd 
 |-  ( ( ph /\ x e. B ) -> ( ( F |` A ) ` ( x - T ) ) = ( F ` ( x - T ) ) )
77 75 76 eqtr4d 
 |-  ( ( ph /\ x e. B ) -> ( F ` ( ( x - T ) + T ) ) = ( ( F |` A ) ` ( x - T ) ) )
78 51 58 77 3eqtrd 
 |-  ( ( ph /\ x e. B ) -> ( ( F |` B ) ` x ) = ( ( F |` A ) ` ( x - T ) ) )
79 78 3adant3 
 |-  ( ( ph /\ x e. B /\ v e. B ) -> ( ( F |` B ) ` x ) = ( ( F |` A ) ` ( x - T ) ) )
80 eleq1 
 |-  ( x = v -> ( x e. B <-> v e. B ) )
81 80 anbi2d 
 |-  ( x = v -> ( ( ph /\ x e. B ) <-> ( ph /\ v e. B ) ) )
82 fveq2 
 |-  ( x = v -> ( ( F |` B ) ` x ) = ( ( F |` B ) ` v ) )
83 fvoveq1 
 |-  ( x = v -> ( ( F |` A ) ` ( x - T ) ) = ( ( F |` A ) ` ( v - T ) ) )
84 82 83 eqeq12d 
 |-  ( x = v -> ( ( ( F |` B ) ` x ) = ( ( F |` A ) ` ( x - T ) ) <-> ( ( F |` B ) ` v ) = ( ( F |` A ) ` ( v - T ) ) ) )
85 81 84 imbi12d 
 |-  ( x = v -> ( ( ( ph /\ x e. B ) -> ( ( F |` B ) ` x ) = ( ( F |` A ) ` ( x - T ) ) ) <-> ( ( ph /\ v e. B ) -> ( ( F |` B ) ` v ) = ( ( F |` A ) ` ( v - T ) ) ) ) )
86 85 78 chvarvv 
 |-  ( ( ph /\ v e. B ) -> ( ( F |` B ) ` v ) = ( ( F |` A ) ` ( v - T ) ) )
87 86 3adant2 
 |-  ( ( ph /\ x e. B /\ v e. B ) -> ( ( F |` B ) ` v ) = ( ( F |` A ) ` ( v - T ) ) )
88 79 87 oveq12d 
 |-  ( ( ph /\ x e. B /\ v e. B ) -> ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) = ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) )
89 88 fveq2d 
 |-  ( ( ph /\ x e. B /\ v e. B ) -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) = ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) ) )
90 45 48 49 89 syl3anc 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) = ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) ) )
91 simpr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( abs ` ( x - v ) ) < z )
92 24 simpld 
 |-  ( ( ph /\ x e. B ) -> x e. CC )
93 92 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ v e. B ) -> x e. CC )
94 52 sseli 
 |-  ( v e. B -> v e. CC )
95 94 adantl 
 |-  ( ( ( ph /\ x e. B ) /\ v e. B ) -> v e. CC )
96 55 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ v e. B ) -> T e. CC )
97 93 95 96 nnncan2d 
 |-  ( ( ( ph /\ x e. B ) /\ v e. B ) -> ( ( x - T ) - ( v - T ) ) = ( x - v ) )
98 97 fveq2d 
 |-  ( ( ( ph /\ x e. B ) /\ v e. B ) -> ( abs ` ( ( x - T ) - ( v - T ) ) ) = ( abs ` ( x - v ) ) )
99 98 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( abs ` ( ( x - T ) - ( v - T ) ) ) = ( abs ` ( x - v ) ) )
100 simpr 
 |-  ( ( ( ( ph /\ x e. B ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( abs ` ( x - v ) ) < z )
101 99 100 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. B ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( abs ` ( ( x - T ) - ( v - T ) ) ) < z )
102 45 48 49 91 101 syl1111anc 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( abs ` ( ( x - T ) - ( v - T ) ) ) < z )
103 oveq2 
 |-  ( b = ( v - T ) -> ( ( x - T ) - b ) = ( ( x - T ) - ( v - T ) ) )
104 103 fveq2d 
 |-  ( b = ( v - T ) -> ( abs ` ( ( x - T ) - b ) ) = ( abs ` ( ( x - T ) - ( v - T ) ) ) )
105 104 breq1d 
 |-  ( b = ( v - T ) -> ( ( abs ` ( ( x - T ) - b ) ) < z <-> ( abs ` ( ( x - T ) - ( v - T ) ) ) < z ) )
106 fveq2 
 |-  ( b = ( v - T ) -> ( ( F |` A ) ` b ) = ( ( F |` A ) ` ( v - T ) ) )
107 106 oveq2d 
 |-  ( b = ( v - T ) -> ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) = ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) )
108 107 fveq2d 
 |-  ( b = ( v - T ) -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) = ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) ) )
109 108 breq1d 
 |-  ( b = ( v - T ) -> ( ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w <-> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) ) < w ) )
110 105 109 imbi12d 
 |-  ( b = ( v - T ) -> ( ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) <-> ( ( abs ` ( ( x - T ) - ( v - T ) ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) ) < w ) ) )
111 simpll3 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) )
112 oveq1 
 |-  ( x = v -> ( x - T ) = ( v - T ) )
113 112 eleq1d 
 |-  ( x = v -> ( ( x - T ) e. A <-> ( v - T ) e. A ) )
114 81 113 imbi12d 
 |-  ( x = v -> ( ( ( ph /\ x e. B ) -> ( x - T ) e. A ) <-> ( ( ph /\ v e. B ) -> ( v - T ) e. A ) ) )
115 114 38 chvarvv 
 |-  ( ( ph /\ v e. B ) -> ( v - T ) e. A )
116 45 49 115 syl2anc 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( v - T ) e. A )
117 110 111 116 rspcdva 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( ( abs ` ( ( x - T ) - ( v - T ) ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) ) < w ) )
118 102 117 mpd 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` ( v - T ) ) ) ) < w )
119 90 118 eqbrtrd 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) /\ ( abs ` ( x - v ) ) < z ) -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w )
120 119 ex 
 |-  ( ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) /\ v e. B ) -> ( ( abs ` ( x - v ) ) < z -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w ) )
121 120 ralrimiva 
 |-  ( ( ( ph /\ ( x e. B /\ w e. RR+ ) ) /\ z e. RR+ /\ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) ) -> A. v e. B ( ( abs ` ( x - v ) ) < z -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w ) )
122 121 3exp 
 |-  ( ( ph /\ ( x e. B /\ w e. RR+ ) ) -> ( z e. RR+ -> ( A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) -> A. v e. B ( ( abs ` ( x - v ) ) < z -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w ) ) ) )
123 122 reximdvai 
 |-  ( ( ph /\ ( x e. B /\ w e. RR+ ) ) -> ( E. z e. RR+ A. b e. A ( ( abs ` ( ( x - T ) - b ) ) < z -> ( abs ` ( ( ( F |` A ) ` ( x - T ) ) - ( ( F |` A ) ` b ) ) ) < w ) -> E. z e. RR+ A. v e. B ( ( abs ` ( x - v ) ) < z -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w ) ) )
124 43 123 mpd 
 |-  ( ( ph /\ ( x e. B /\ w e. RR+ ) ) -> E. z e. RR+ A. v e. B ( ( abs ` ( x - v ) ) < z -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w ) )
125 124 ralrimivva 
 |-  ( ph -> A. x e. B A. w e. RR+ E. z e. RR+ A. v e. B ( ( abs ` ( x - v ) ) < z -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w ) )
126 52 a1i 
 |-  ( ph -> B C_ CC )
127 ssidd 
 |-  ( ph -> CC C_ CC )
128 elcncf 
 |-  ( ( B C_ CC /\ CC C_ CC ) -> ( ( F |` B ) e. ( B -cn-> CC ) <-> ( ( F |` B ) : B --> CC /\ A. x e. B A. w e. RR+ E. z e. RR+ A. v e. B ( ( abs ` ( x - v ) ) < z -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w ) ) ) )
129 126 127 128 syl2anc 
 |-  ( ph -> ( ( F |` B ) e. ( B -cn-> CC ) <-> ( ( F |` B ) : B --> CC /\ A. x e. B A. w e. RR+ E. z e. RR+ A. v e. B ( ( abs ` ( x - v ) ) < z -> ( abs ` ( ( ( F |` B ) ` x ) - ( ( F |` B ) ` v ) ) ) < w ) ) ) )
130 8 125 129 mpbir2and 
 |-  ( ph -> ( F |` B ) e. ( B -cn-> CC ) )