fourierdlem96

Description: limit for F at the lower bound of an interval for the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem96.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem96.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))\})$
	fourierdlem96.t	$⊢ T = B - A$
	fourierdlem96.m	$⊢ φ \to M \in ℕ$
	fourierdlem96.q	$⊢ φ \to Q \in P (M)$
	fourierdlem96.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem96.qcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem96.8	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem96.c	$⊢ φ \to C \in ℝ$
	fourierdlem96.d	$⊢ φ \to D \in (C, +∞)$
	fourierdlem96.j	$⊢ φ \to J \in (0 ..^\|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
	fourierdlem96.v	$⊢ V = (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}))$
Assertion	fourierdlem96	$⊢ φ \to if ((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))) = Q ((y \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} ℝ <)) (V (J))), (i \in (0 ..^M) ⟼ R) ((y \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} ℝ <)) (V (J))), F ((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))))) \in (({F ↾}_{(V (J), V (J + 1))}) {lim}_{ℂ} V (J))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem96.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem96.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))\})$
3		fourierdlem96.t	$⊢ T = B - A$
4		fourierdlem96.m	$⊢ φ \to M \in ℕ$
5		fourierdlem96.q	$⊢ φ \to Q \in P (M)$
6		fourierdlem96.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
7		fourierdlem96.qcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
8		fourierdlem96.8	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
9		fourierdlem96.c	$⊢ φ \to C \in ℝ$
10		fourierdlem96.d	$⊢ φ \to D \in (C, +∞)$
11		fourierdlem96.j	$⊢ φ \to J \in (0 ..^\|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
12		fourierdlem96.v	$⊢ V = (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}))$
13		ax-resscn	$⊢ ℝ \subseteq ℂ$
14	13	a1i	$⊢ φ \to ℝ \subseteq ℂ$
15	1 14	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
16		eqid	$⊢ (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
17		oveq1	$⊢ z = y \to z + l T = y + l T$
18	17	eleq1d	$⊢ z = y \to (z + l T \in ran Q \leftrightarrow y + l T \in ran Q)$
19	18	rexbidv	$⊢ z = y \to (\exists l \in ℤ z + l T \in ran Q \leftrightarrow \exists l \in ℤ y + l T \in ran Q)$
20	19	cbvrabv	$⊢ \{z \in [C, D] \| \exists l \in ℤ z + l T \in ran Q\} = \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}$
21	20	uneq2i	$⊢ \{C, D\} \cup \{z \in [C, D] \| \exists l \in ℤ z + l T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}$
22	21	eqcomi	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\} = \{C, D\} \cup \{z \in [C, D] \| \exists l \in ℤ z + l T \in ran Q\}$
23		oveq1	$⊢ k = l \to k T = l T$
24	23	oveq2d	$⊢ k = l \to y + k T = y + l T$
25	24	eleq1d	$⊢ k = l \to (y + k T \in ran Q \leftrightarrow y + l T \in ran Q)$
26	25	cbvrexvw	$⊢ \exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists l \in ℤ y + l T \in ran Q$
27	26	a1i	$⊢ y \in [C, D] \to (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists l \in ℤ y + l T \in ran Q)$
28	27	rabbiia	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}$
29	28	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}$
30	29	fveq2i	$⊢ \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| = \|\{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}\|$
31	30	oveq1i	$⊢ \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1 = \|\{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}\| - 1$
32		oveq1	$⊢ l = h \to l T = h T$
33	32	oveq2d	$⊢ l = h \to y + l T = y + h T$
34	33	eleq1d	$⊢ l = h \to (y + l T \in ran Q \leftrightarrow y + h T \in ran Q)$
35	34	cbvrexvw	$⊢ \exists l \in ℤ y + l T \in ran Q \leftrightarrow \exists h \in ℤ y + h T \in ran Q$
36	35	a1i	$⊢ y \in [C, D] \to (\exists l \in ℤ y + l T \in ran Q \leftrightarrow \exists h \in ℤ y + h T \in ran Q)$
37	36	rabbiia	$⊢ \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\} = \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}$
38	37	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}$
39		isoeq5	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\} \to (g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}))$
40	38 39	ax-mp	$⊢ g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\})$
41	40	iotabii	$⊢ (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\})) = (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists h \in ℤ y + h T \in ran Q\}))$
42		isoeq1	$⊢ f = g \to (f {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}))$
43	42	cbviotavw	$⊢ (ι f \| f {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\})) = (ι g \| g {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}))$
44	41 43 12	3eqtr4ri	$⊢ V = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{C, D\} \cup \{y \in [C, D] \| \exists l \in ℤ y + l T \in ran Q\}))$
45		id	$⊢ v = x \to v = x$
46		oveq2	$⊢ v = x \to B - v = B - x$
47	46	oveq1d	$⊢ v = x \to \frac{B - v}{T} = \frac{B - x}{T}$
48	47	fveq2d	$⊢ v = x \to ⌊\frac{B - v}{T}⌋ = ⌊\frac{B - x}{T}⌋$
49	48	oveq1d	$⊢ v = x \to ⌊\frac{B - v}{T}⌋ T = ⌊\frac{B - x}{T}⌋ T$
50	45 49	oveq12d	$⊢ v = x \to v + ⌊\frac{B - v}{T}⌋ T = x + ⌊\frac{B - x}{T}⌋ T$
51	50	cbvmptv	$⊢ (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
52		eqeq1	$⊢ u = z \to (u = B \leftrightarrow z = B)$
53		id	$⊢ u = z \to u = z$
54	52 53	ifbieq2d	$⊢ u = z \to if (u = B, A, u) = if (z = B, A, z)$
55	54	cbvmptv	$⊢ (u \in (A, B] ⟼ if (u = B, A, u)) = (z \in (A, B] ⟼ if (z = B, A, z))$
56		eqid	$⊢ V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1)) = V (J + 1) - (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J + 1))$
57		fveq2	$⊢ j = i \to Q (j) = Q (i)$
58	57	breq1d	$⊢ j = i \to (Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y)) \leftrightarrow Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y)))$
59	58	cbvrabv	$⊢ \{j \in (0 ..^M) \| Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} = \{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\}$
60		fveq2	$⊢ y = x \to (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y) = (v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x)$
61	60	fveq2d	$⊢ y = x \to (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y)) = (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))$
62	61	breq2d	$⊢ y = x \to (Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y)) \leftrightarrow Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x)))$
63	62	rabbidv	$⊢ y = x \to \{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} = \{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\}$
64	59 63	syl5eq	$⊢ y = x \to \{j \in (0 ..^M) \| Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} = \{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\}$
65	64	supeq1d	$⊢ y = x \to sup (\{j \in (0 ..^M) \| Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} ℝ <) = sup (\{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\} ℝ <)$
66	65	cbvmptv	$⊢ (y \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} ℝ <)) = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (x))\} ℝ <))$
67		eqid	$⊢ (i \in (0 ..^M) ⟼ R) = (i \in (0 ..^M) ⟼ R)$
68	2 3 4 5 15 6 7 8 9 10 16 22 31 44 51 55 11 56 66 67	fourierdlem89	$⊢ φ \to if ((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))) = Q ((y \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} ℝ <)) (V (J))), (i \in (0 ..^M) ⟼ R) ((y \in ℝ ⟼ sup (\{j \in (0 ..^M) \| Q (j) \leq (u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (y))\} ℝ <)) (V (J))), F ((u \in (A, B] ⟼ if (u = B, A, u)) ((v \in ℝ ⟼ v + ⌊\frac{B - v}{T}⌋ T) (V (J))))) \in (({F ↾}_{(V (J), V (J + 1))}) {lim}_{ℂ} V (J))$

Metamath Proof Explorer

Theorem fourierdlem96

Proof