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 φ A
cncfshift.t φ T
cncfshift.b B = x | y A x = y + T
cncfshift.f φ F : A cn
cncfshift.g G = x B F x T
Assertion cncfshift φ G : B cn

Proof

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