Metamath Proof Explorer

Theorem cncfshift

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

Ref Expression
Hypotheses cncfshift.a 
|- ( ph -> A C_ CC )
cncfshift.t 
|- ( ph -> T e. CC )
cncfshift.b 
|- B = { x e. CC | E. y e. A x = ( y + T ) }
cncfshift.f 
|- ( ph -> F e. ( A -cn-> CC ) )
cncfshift.g 
|- G = ( x e. B |-> ( F ` ( x - T ) ) )
Assertion cncfshift 
|- ( ph -> G e. ( B -cn-> CC ) )

Proof

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