fourierdlem98

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem98.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem98.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))\})$
	fourierdlem98.t	$⊢ T = B - A$
	fourierdlem98.m	$⊢ φ \to M \in ℕ$
	fourierdlem98.q	$⊢ φ \to Q \in P (M)$
	fourierdlem98.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem98.qcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem98.c	$⊢ φ \to C \in ℝ$
	fourierdlem98.d	$⊢ φ \to D \in (C, +∞)$
	fourierdlem98.j	$⊢ φ \to J \in (0 ..^\|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
	fourierdlem98.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	fourierdlem98	$⊢ φ \to ({F ↾}_{(V (J), V (J + 1))}) : (V (J), V (J + 1)) \underset{cn}{⟶} ℂ$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem98

Proof