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	$⊢ φ \to A \subseteq ℂ$
	cncfshift.t	$⊢ φ \to T \in ℂ$
	cncfshift.b	$⊢ B = \{x \in ℂ \| \exists y \in A x = y + T\}$
	cncfshift.f	$⊢ φ \to F : A \underset{cn}{⟶} ℂ$
	cncfshift.g	$⊢ G = (x \in B ⟼ F (x - T))$
Assertion	cncfshift	$⊢ φ \to G : B \underset{cn}{⟶} ℂ$

Proof

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

Metamath Proof Explorer

Theorem cncfshift

Proof