fourierdlem109

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem109.a	$⊢ φ \to A \in ℝ$
	fourierdlem109.b	$⊢ φ \to B \in ℝ$
	fourierdlem109.t	$⊢ T = B - A$
	fourierdlem109.x	$⊢ φ \to X \in ℝ$
	fourierdlem109.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem109.m	$⊢ φ \to M \in ℕ$
	fourierdlem109.q	$⊢ φ \to Q \in P (M)$
	fourierdlem109.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	fourierdlem109.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem109.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem109.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem109.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem109.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = B - X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem109.h	$⊢ H = \{A - X, B - X\} \cup \{x \in [A - X, B - X] \| \exists k \in ℤ x + k T \in ran Q\}$
	fourierdlem109.n	$⊢ N = \|H\| - 1$
	fourierdlem109.16	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
	fourierdlem109.17	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem109.18	$⊢ J = (y \in (A, B] ⟼ if (y = B, A, y))$
	fourierdlem109.19	$⊢ I = (x \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq J (E (x))\} ℝ <))$
Assertion	fourierdlem109	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem109.a	$⊢ φ \to A \in ℝ$
2		fourierdlem109.b	$⊢ φ \to B \in ℝ$
3		fourierdlem109.t	$⊢ T = B - A$
4		fourierdlem109.x	$⊢ φ \to X \in ℝ$
5		fourierdlem109.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
6		fourierdlem109.m	$⊢ φ \to M \in ℕ$
7		fourierdlem109.q	$⊢ φ \to Q \in P (M)$
8		fourierdlem109.f	$⊢ φ \to F : ℝ ⟶ ℂ$
9		fourierdlem109.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
10		fourierdlem109.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
11		fourierdlem109.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
12		fourierdlem109.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
13		fourierdlem109.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = B - X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
14		fourierdlem109.h	$⊢ H = \{A - X, B - X\} \cup \{x \in [A - X, B - X] \| \exists k \in ℤ x + k T \in ran Q\}$
15		fourierdlem109.n	$⊢ N = \|H\| - 1$
16		fourierdlem109.16	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
17		fourierdlem109.17	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
18		fourierdlem109.18	$⊢ J = (y \in (A, B] ⟼ if (y = B, A, y))$
19		fourierdlem109.19	$⊢ I = (x \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq J (E (x))\} ℝ <))$
20	1	adantr	$⊢ (φ \land 0 < X) \to A \in ℝ$
21	2	adantr	$⊢ (φ \land 0 < X) \to B \in ℝ$
22	4	adantr	$⊢ (φ \land 0 < X) \to X \in ℝ$
23		simpr	$⊢ (φ \land 0 < X) \to 0 < X$
24	22 23	elrpd	$⊢ (φ \land 0 < X) \to X \in ℝ^{+}$
25	6	adantr	$⊢ (φ \land 0 < X) \to M \in ℕ$
26	7	adantr	$⊢ (φ \land 0 < X) \to Q \in P (M)$
27	8	adantr	$⊢ (φ \land 0 < X) \to F : ℝ ⟶ ℂ$
28	9	adantlr	$⊢ ((φ \land 0 < X) \land x \in ℝ) \to F (x + T) = F (x)$
29	10	adantlr	$⊢ ((φ \land 0 < X) \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
30	11	adantlr	$⊢ ((φ \land 0 < X) \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
31	12	adantlr	$⊢ ((φ \land 0 < X) \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
32	20 21 3 24 5 25 26 27 28 29 30 31	fourierdlem108	$⊢ (φ \land 0 < X) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$
33		oveq2	$⊢ X = 0 \to A - X = A - 0$
34	1	recnd	$⊢ φ \to A \in ℂ$
35	34	subid1d	$⊢ φ \to A - 0 = A$
36	33 35	sylan9eqr	$⊢ (φ \land X = 0) \to A - X = A$
37		oveq2	$⊢ X = 0 \to B - X = B - 0$
38	2	recnd	$⊢ φ \to B \in ℂ$
39	38	subid1d	$⊢ φ \to B - 0 = B$
40	37 39	sylan9eqr	$⊢ (φ \land X = 0) \to B - X = B$
41	36 40	oveq12d	$⊢ (φ \land X = 0) \to [A - X, B - X] = [A, B]$
42	41	itgeq1d	$⊢ (φ \land X = 0) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$
43	42	adantlr	$⊢ ((φ \land \neg 0 < X) \land X = 0) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$
44		simpll	$⊢ ((φ \land \neg 0 < X) \land \neg X = 0) \to φ$
45	44 4	syl	$⊢ ((φ \land \neg 0 < X) \land \neg X = 0) \to X \in ℝ$
46		0red	$⊢ ((φ \land \neg 0 < X) \land \neg X = 0) \to 0 \in ℝ$
47		simpr	$⊢ ((φ \land \neg 0 < X) \land \neg X = 0) \to \neg X = 0$
48	47	neqned	$⊢ ((φ \land \neg 0 < X) \land \neg X = 0) \to X \neq 0$
49		simplr	$⊢ ((φ \land \neg 0 < X) \land \neg X = 0) \to \neg 0 < X$
50	45 46 48 49	lttri5d	$⊢ ((φ \land \neg 0 < X) \land \neg X = 0) \to X < 0$
51	4	recnd	$⊢ φ \to X \in ℂ$
52	34 51	subcld	$⊢ φ \to A - X \in ℂ$
53	52 51	subnegd	$⊢ φ \to A - X - (- X) = A - X + X$
54	34 51	npcand	$⊢ φ \to A - X + X = A$
55	53 54	eqtrd	$⊢ φ \to A - X - (- X) = A$
56	38 51	subcld	$⊢ φ \to B - X \in ℂ$
57	56 51	subnegd	$⊢ φ \to B - X - (- X) = B - X + X$
58	38 51	npcand	$⊢ φ \to B - X + X = B$
59	57 58	eqtrd	$⊢ φ \to B - X - (- X) = B$
60	55 59	oveq12d	$⊢ φ \to [A - X - (- X), B - X - (- X)] = [A, B]$
61	60	eqcomd	$⊢ φ \to [A, B] = [A - X - (- X), B - X - (- X)]$
62	61	itgeq1d	$⊢ φ \to \int_{[A, B]} F (x) d x = \int_{[A - X - (- X), B - X - (- X)]} F (x) d x$
63	62	adantr	$⊢ (φ \land X < 0) \to \int_{[A, B]} F (x) d x = \int_{[A - X - (- X), B - X - (- X)]} F (x) d x$
64	1 4	resubcld	$⊢ φ \to A - X \in ℝ$
65	64	adantr	$⊢ (φ \land X < 0) \to A - X \in ℝ$
66	2 4	resubcld	$⊢ φ \to B - X \in ℝ$
67	66	adantr	$⊢ (φ \land X < 0) \to B - X \in ℝ$
68		eqid	$⊢ B - X - (A - X) = B - X - (A - X)$
69	4	renegcld	$⊢ φ \to - X \in ℝ$
70	69	adantr	$⊢ (φ \land X < 0) \to - X \in ℝ$
71	4	lt0neg1d	$⊢ φ \to (X < 0 \leftrightarrow 0 < - X)$
72	71	biimpa	$⊢ (φ \land X < 0) \to 0 < - X$
73	70 72	elrpd	$⊢ (φ \land X < 0) \to - X \in ℝ^{+}$
74		fveq2	$⊢ i = j \to p (i) = p (j)$
75		oveq1	$⊢ i = j \to i + 1 = j + 1$
76	75	fveq2d	$⊢ i = j \to p (i + 1) = p (j + 1)$
77	74 76	breq12d	$⊢ i = j \to (p (i) < p (i + 1) \leftrightarrow p (j) < p (j + 1))$
78	77	cbvralvw	$⊢ \forall i \in (0 ..^m) p (i) < p (i + 1) \leftrightarrow \forall j \in (0 ..^m) p (j) < p (j + 1)$
79	78	anbi2i	$⊢ ((p (0) = A - X \land p (m) = B - X) \land \forall i \in (0 ..^m) p (i) < p (i + 1)) \leftrightarrow ((p (0) = A - X \land p (m) = B - X) \land \forall j \in (0 ..^m) p (j) < p (j + 1))$
80	79	a1i	$⊢ p \in (ℝ^{(0 \dots m)}) \to (((p (0) = A - X \land p (m) = B - X) \land \forall i \in (0 ..^m) p (i) < p (i + 1)) \leftrightarrow ((p (0) = A - X \land p (m) = B - X) \land \forall j \in (0 ..^m) p (j) < p (j + 1)))$
81	80	rabbiia	$⊢ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = B - X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\} = \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = B - X) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\}$
82	81	mpteq2i	$⊢ (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = B - X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = B - X) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\})$
83	13 82	eqtri	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A - X \land p (m) = B - X) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\})$
84	5 6 7	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
85	84	simp3d	$⊢ φ \to A < B$
86	1 2 4 85	ltsub1dd	$⊢ φ \to A - X < B - X$
87	3 5 6 7 64 66 86 13 14 15 16	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), H))$
88	87	simpld	$⊢ φ \to (N \in ℕ \land S \in O (N))$
89	88	simpld	$⊢ φ \to N \in ℕ$
90	89	adantr	$⊢ (φ \land X < 0) \to N \in ℕ$
91	88	simprd	$⊢ φ \to S \in O (N)$
92	91	adantr	$⊢ (φ \land X < 0) \to S \in O (N)$
93	8	adantr	$⊢ (φ \land X < 0) \to F : ℝ ⟶ ℂ$
94	38 34 51	nnncan2d	$⊢ φ \to B - X - (A - X) = B - A$
95	94 3	eqtr4di	$⊢ φ \to B - X - (A - X) = T$
96	95	oveq2d	$⊢ φ \to x + (B - X) - (A - X) = x + T$
97	96	adantr	$⊢ (φ \land x \in ℝ) \to x + (B - X) - (A - X) = x + T$
98	97	fveq2d	$⊢ (φ \land x \in ℝ) \to F (x + (B - X) - (A - X)) = F (x + T)$
99	98 9	eqtrd	$⊢ (φ \land x \in ℝ) \to F (x + (B - X) - (A - X)) = F (x)$
100	99	adantlr	$⊢ ((φ \land X < 0) \land x \in ℝ) \to F (x + (B - X) - (A - X)) = F (x)$
101	6	adantr	$⊢ (φ \land j \in (0 ..^N)) \to M \in ℕ$
102	7	adantr	$⊢ (φ \land j \in (0 ..^N)) \to Q \in P (M)$
103	8	adantr	$⊢ (φ \land j \in (0 ..^N)) \to F : ℝ ⟶ ℂ$
104	9	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land x \in ℝ) \to F (x + T) = F (x)$
105	10	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
106	64	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A - X \in ℝ$
107	64	rexrd	$⊢ φ \to A - X \in ℝ^{*}$
108		pnfxr	$⊢ +∞ \in ℝ^{*}$
109	108	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
110	66	ltpnfd	$⊢ φ \to B - X < +∞$
111	107 109 66 86 110	eliood	$⊢ φ \to B - X \in (A - X, +∞)$
112	111	adantr	$⊢ (φ \land j \in (0 ..^N)) \to B - X \in (A - X, +∞)$
113		oveq1	$⊢ x = y \to x + k T = y + k T$
114	113	eleq1d	$⊢ x = y \to (x + k T \in ran Q \leftrightarrow y + k T \in ran Q)$
115	114	rexbidv	$⊢ x = y \to (\exists k \in ℤ x + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k T \in ran Q)$
116	115	cbvrabv	$⊢ \{x \in [A - X, B - X] \| \exists k \in ℤ x + k T \in ran Q\} = \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}$
117	116	uneq2i	$⊢ \{A - X, B - X\} \cup \{x \in [A - X, B - X] \| \exists k \in ℤ x + k T \in ran Q\} = \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}$
118	14 117	eqtri	$⊢ H = \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}$
119		simpr	$⊢ (φ \land j \in (0 ..^N)) \to j \in (0 ..^N)$
120		eqid	$⊢ S (j + 1) - E (S (j + 1)) = S (j + 1) - E (S (j + 1))$
121		eqid	$⊢ {F ↾}_{(J (E (S (j))), E (S (j + 1)))} = {F ↾}_{(J (E (S (j))), E (S (j + 1)))}$
122		eqid	$⊢ (y \in (J (E (S (j))) + S (j + 1) - E (S (j + 1)), E (S (j + 1)) + S (j + 1) - E (S (j + 1))) ⟼ ({F ↾}_{(J (E (S (j))), E (S (j + 1)))}) (y - (S (j + 1) - E (S (j + 1))))) = (y \in (J (E (S (j))) + S (j + 1) - E (S (j + 1)), E (S (j + 1)) + S (j + 1) - E (S (j + 1))) ⟼ ({F ↾}_{(J (E (S (j))), E (S (j + 1)))}) (y - (S (j + 1) - E (S (j + 1)))))$
123		fveq2	$⊢ j = i \to Q (j) = Q (i)$
124	123	breq1d	$⊢ j = i \to (Q (j) \leq J (E (x)) \leftrightarrow Q (i) \leq J (E (x)))$
125	124	cbvrabv	$⊢ \{j \in (0 ..^M) \| Q (j) \leq J (E (x))\} = \{i \in (0 ..^M) \| Q (i) \leq J (E (x))\}$
126	125	supeq1i	$⊢ sup (\{j \in (0 ..^M) \| Q (j) \leq J (E (x))\} ℝ <) = sup (\{i \in (0 ..^M) \| Q (i) \leq J (E (x))\} ℝ <)$
127	126	mpteq2i	$⊢ (x \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq J (E (x))\} ℝ <)) = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq J (E (x))\} ℝ <))$
128	19 127	eqtri	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq J (E (x))\} ℝ <))$
129	5 3 101 102 103 104 105 106 112 13 118 15 16 17 18 119 120 121 122 128	fourierdlem90	$⊢ (φ \land j \in (0 ..^N)) \to ({F ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ$
130	129	adantlr	$⊢ ((φ \land X < 0) \land j \in (0 ..^N)) \to ({F ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ$
131	11	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
132		eqid	$⊢ (i \in (0 ..^M) ⟼ R) = (i \in (0 ..^M) ⟼ R)$
133	5 3 101 102 103 104 105 131 106 112 13 118 15 16 17 18 119 120 128 132	fourierdlem89	$⊢ (φ \land j \in (0 ..^N)) \to if (J (E (S (j))) = Q (I (S (j))), (i \in (0 ..^M) ⟼ R) (I (S (j))), F (J (E (S (j))))) \in (({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))$
134	133	adantlr	$⊢ ((φ \land X < 0) \land j \in (0 ..^N)) \to if (J (E (S (j))) = Q (I (S (j))), (i \in (0 ..^M) ⟼ R) (I (S (j))), F (J (E (S (j))))) \in (({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))$
135	12	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
136		eqid	$⊢ (i \in (0 ..^M) ⟼ L) = (i \in (0 ..^M) ⟼ L)$
137	5 3 101 102 103 104 105 135 106 112 13 118 15 16 17 18 119 120 128 136	fourierdlem91	$⊢ (φ \land j \in (0 ..^N)) \to if (E (S (j + 1)) = Q (I (S (j)) + 1), (i \in (0 ..^M) ⟼ L) (I (S (j))), F (E (S (j + 1)))) \in (({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1))$
138	137	adantlr	$⊢ ((φ \land X < 0) \land j \in (0 ..^N)) \to if (E (S (j + 1)) = Q (I (S (j)) + 1), (i \in (0 ..^M) ⟼ L) (I (S (j))), F (E (S (j + 1)))) \in (({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1))$
139	65 67 68 73 83 90 92 93 100 130 134 138	fourierdlem108	$⊢ (φ \land X < 0) \to \int_{[A - X - (- X), B - X - (- X)]} F (x) d x = \int_{[A - X, B - X]} F (x) d x$
140	63 139	eqtr2d	$⊢ (φ \land X < 0) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$
141	44 50 140	syl2anc	$⊢ ((φ \land \neg 0 < X) \land \neg X = 0) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$
142	43 141	pm2.61dan	$⊢ (φ \land \neg 0 < X) \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$
143	32 142	pm2.61dan	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$

Metamath Proof Explorer

Theorem fourierdlem109

Proof