fourierdlem110

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	fourierdlem110.a	$⊢ φ \to A \in ℝ$
	fourierdlem110.b	$⊢ φ \to B \in ℝ$
	fourierdlem110.t	$⊢ T = B - A$
	fourierdlem110.x	$⊢ φ \to X \in ℝ$
	fourierdlem110.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))\})$
	fourierdlem110.m	$⊢ φ \to M \in ℕ$
	fourierdlem110.q	$⊢ φ \to Q \in P (M)$
	fourierdlem110.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	fourierdlem110.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem110.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem110.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem110.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
Assertion	fourierdlem110	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem110.a	$⊢ φ \to A \in ℝ$
2		fourierdlem110.b	$⊢ φ \to B \in ℝ$
3		fourierdlem110.t	$⊢ T = B - A$
4		fourierdlem110.x	$⊢ φ \to X \in ℝ$
5		fourierdlem110.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		fourierdlem110.m	$⊢ φ \to M \in ℕ$
7		fourierdlem110.q	$⊢ φ \to Q \in P (M)$
8		fourierdlem110.f	$⊢ φ \to F : ℝ ⟶ ℂ$
9		fourierdlem110.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
10		fourierdlem110.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
11		fourierdlem110.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
12		fourierdlem110.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
13		eqid	$⊢ (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 i \in (0 ..^m) p (i) < p (i + 1))\})$
14		oveq1	$⊢ y = x \to y + k T = x + k T$
15	14	eleq1d	$⊢ y = x \to (y + k T \in ran Q \leftrightarrow x + k T \in ran Q)$
16	15	rexbidv	$⊢ y = x \to (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ x + k T \in ran Q)$
17	16	cbvrabv	$⊢ \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\} = \{x \in [A - X, B - X] \| \exists k \in ℤ x + k T \in ran Q\}$
18	17	uneq2i	$⊢ \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\} = \{A - X, B - X\} \cup \{x \in [A - X, B - X] \| \exists k \in ℤ x + k T \in ran Q\}$
19		oveq1	$⊢ l = k \to l T = k T$
20	19	oveq2d	$⊢ l = k \to y + l T = y + k T$
21	20	eleq1d	$⊢ l = k \to (y + l T \in ran Q \leftrightarrow y + k T \in ran Q)$
22	21	cbvrexvw	$⊢ \exists l \in ℤ y + l T \in ran Q \leftrightarrow \exists k \in ℤ y + k T \in ran Q$
23	22	a1i	$⊢ y \in [A - X, B - X] \to (\exists l \in ℤ y + l T \in ran Q \leftrightarrow \exists k \in ℤ y + k T \in ran Q)$
24	23	rabbiia	$⊢ \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\} = \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}$
25	24	uneq2i	$⊢ \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\} = \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}$
26	25	fveq2i	$⊢ \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| = \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}\|$
27	26	oveq1i	$⊢ \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1 = \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1$
28		isoeq5	$⊢ \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\} = \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\} \to (g {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}))$
29	25 28	ax-mp	$⊢ g {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\})$
30		isoeq1	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}))$
31	29 30	bitrid	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}))$
32	31	cbviotavw	$⊢ (ι g \| g {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\})) = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1), \{A - X, B - X\} \cup \{y \in [A - X, B - X] \| \exists k \in ℤ y + k T \in ran Q\}))$
33		id	$⊢ y = x \to y = x$
34		oveq2	$⊢ y = x \to B - y = B - x$
35	34	oveq1d	$⊢ y = x \to \frac{B - y}{T} = \frac{B - x}{T}$
36	35	fveq2d	$⊢ y = x \to ⌊\frac{B - y}{T}⌋ = ⌊\frac{B - x}{T}⌋$
37	36	oveq1d	$⊢ y = x \to ⌊\frac{B - y}{T}⌋ T = ⌊\frac{B - x}{T}⌋ T$
38	33 37	oveq12d	$⊢ y = x \to y + ⌊\frac{B - y}{T}⌋ T = x + ⌊\frac{B - x}{T}⌋ T$
39	38	cbvmptv	$⊢ (y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
40		eqeq1	$⊢ y = w \to (y = B \leftrightarrow w = B)$
41		id	$⊢ y = w \to y = w$
42	40 41	ifbieq2d	$⊢ y = w \to if (y = B, A, y) = if (w = B, A, w)$
43	42	cbvmptv	$⊢ (y \in (A, B] ⟼ if (y = B, A, y)) = (w \in (A, B] ⟼ if (w = B, A, w))$
44		fveq2	$⊢ z = x \to (y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (z) = (y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (x)$
45	44	fveq2d	$⊢ z = x \to (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (z)) = (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (x))$
46	45	breq2d	$⊢ z = x \to (Q (j) \leq (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (z)) \leftrightarrow Q (j) \leq (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (x)))$
47	46	rabbidv	$⊢ z = x \to \{j \in (0 ..^M) \| Q (j) \leq (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (z))\} = \{j \in (0 ..^M) \| Q (j) \leq (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (x))\}$
48	47	supeq1d	$⊢ z = x \to sup (\{j \in (0 ..^M) \| Q (j) \leq (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (z))\} ℝ <) = sup (\{j \in (0 ..^M) \| Q (j) \leq (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (x))\} ℝ <)$
49	48	cbvmptv	$⊢ (z \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (z))\} ℝ <)) = (x \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq (y \in (A, B] ⟼ if (y = B, A, y)) ((y \in ℝ ⟼ y + ⌊\frac{B - y}{T}⌋ T) (x))\} ℝ <))$
50	1 2 3 4 5 6 7 8 9 10 11 12 13 18 27 32 39 43 49	fourierdlem109	$⊢ φ \to \int_{[A - X, B - X]} F (x) d x = \int_{[A, B]} F (x) d x$

Metamath Proof Explorer

Theorem fourierdlem110

Proof