Metamath Proof Explorer

Theorem fourierdlem108

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any positive 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 fourierdlem108.a ⊢ φ → A ∈ ℝ
fourierdlem108.b ⊢ φ → B ∈ ℝ
fourierdlem108.t ⊢ T = B − A
fourierdlem108.x ⊢ φ → X ∈ ℝ +
fourierdlem108.p ⊢ P = m ∈ ℕ ⟼ p ∈ ℝ 0 … m | p ⁡ 0 = A ∧ p ⁡ m = B ∧ ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1
fourierdlem108.m ⊢ φ → M ∈ ℕ
fourierdlem108.q ⊢ φ → Q ∈ P ⁡ M
fourierdlem108.f ⊢ φ → F : ℝ ⟶ ℂ
fourierdlem108.fper ⊢ φ ∧ x ∈ ℝ → F ⁡ x + T = F ⁡ x
fourierdlem108.fcn ⊢ φ ∧ i ∈ 0 ..^ M → F ↾ Q ⁡ i Q ⁡ i + 1 : Q ⁡ i Q ⁡ i + 1 ⟶cn ℂ
fourierdlem108.r ⊢ φ ∧ i ∈ 0 ..^ M → R ∈ F ↾ Q ⁡ i Q ⁡ i + 1 lim ℂ Q ⁡ i
fourierdlem108.l ⊢ φ ∧ i ∈ 0 ..^ M → L ∈ F ↾ Q ⁡ i Q ⁡ i + 1 lim ℂ Q ⁡ i + 1
Assertion fourierdlem108 ⊢ φ → ∫ A − X B − X F ⁡ x dx = ∫ A B F ⁡ x dx

Proof

Step Hyp Ref Expression
1 fourierdlem108.a ⊢ φ → A ∈ ℝ
2 fourierdlem108.b ⊢ φ → B ∈ ℝ
3 fourierdlem108.t ⊢ T = B − A
4 fourierdlem108.x ⊢ φ → X ∈ ℝ +
5 fourierdlem108.p ⊢ P = m ∈ ℕ ⟼ p ∈ ℝ 0 … m | p ⁡ 0 = A ∧ p ⁡ m = B ∧ ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1
6 fourierdlem108.m ⊢ φ → M ∈ ℕ
7 fourierdlem108.q ⊢ φ → Q ∈ P ⁡ M
8 fourierdlem108.f ⊢ φ → F : ℝ ⟶ ℂ
9 fourierdlem108.fper ⊢ φ ∧ x ∈ ℝ → F ⁡ x + T = F ⁡ x
10 fourierdlem108.fcn ⊢ φ ∧ i ∈ 0 ..^ M → F ↾ Q ⁡ i Q ⁡ i + 1 : Q ⁡ i Q ⁡ i + 1 ⟶cn ℂ
11 fourierdlem108.r ⊢ φ ∧ i ∈ 0 ..^ M → R ∈ F ↾ Q ⁡ i Q ⁡ i + 1 lim ℂ Q ⁡ i
12 fourierdlem108.l ⊢ φ ∧ i ∈ 0 ..^ M → L ∈ F ↾ Q ⁡ i Q ⁡ i + 1 lim ℂ Q ⁡ i + 1
13 eqid ⊢ m ∈ ℕ ⟼ p ∈ ℝ 0 … m | p ⁡ 0 = A − X ∧ p ⁡ m = A ∧ ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1 = m ∈ ℕ ⟼ p ∈ ℝ 0 … m | p ⁡ 0 = A − X ∧ p ⁡ m = A ∧ ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1
14 oveq1 ⊢ w = y → w + k ⁢ T = y + k ⁢ T
15 14 eleq1d ⊢ w = y → w + k ⁢ T ∈ ran ⁡ Q ↔ y + k ⁢ T ∈ ran ⁡ Q
16 15 rexbidv ⊢ w = y → ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q ↔ ∃ k ∈ ℤ y + k ⁢ T ∈ ran ⁡ Q
17 16 cbvrabv ⊢ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q = y ∈ A − X A | ∃ k ∈ ℤ y + k ⁢ T ∈ ran ⁡ Q
18 17 uneq2i ⊢ A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q = A − X A ∪ y ∈ A − X A | ∃ k ∈ ℤ y + k ⁢ T ∈ ran ⁡ Q
19 oveq1 ⊢ l = k → l ⁢ T = k ⁢ T
20 19 oveq2d ⊢ l = k → w + l ⁢ T = w + k ⁢ T
21 20 eleq1d ⊢ l = k → w + l ⁢ T ∈ ran ⁡ Q ↔ w + k ⁢ T ∈ ran ⁡ Q
22 21 cbvrexvw ⊢ ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q ↔ ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
23 22 rgenw ⊢ ∀ w ∈ A − X A ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q ↔ ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
24 rabbi ⊢ ∀ w ∈ A − X A ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q ↔ ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q ↔ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q = w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
25 23 24 mpbi ⊢ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q = w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
26 25 uneq2i ⊢ A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q = A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
27 26 fveq2i ⊢ A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q = A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
28 27 oveq1i ⊢ A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 = A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q − 1
29 isoeq5 ⊢ A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q = A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q → g Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q ↔ g Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
30 26 29 ax-mp ⊢ g Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q ↔ g Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
31 isoeq1 ⊢ g = f → g Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q ↔ f Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
32 30 31 syl5bb ⊢ g = f → g Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q ↔ f Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
33 32 cbviotavw ⊢ ι g | g Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q = ι f | f Isom < , < 0 … A − X A ∪ w ∈ A − X A | ∃ l ∈ ℤ w + l ⁢ T ∈ ran ⁡ Q − 1 A − X A ∪ w ∈ A − X A | ∃ k ∈ ℤ w + k ⁢ T ∈ ran ⁡ Q
34 id ⊢ w = x → w = x
35 oveq2 ⊢ w = x → B − w = B − x
36 35 oveq1d ⊢ w = x → B − w T = B − x T
37 36 fveq2d ⊢ w = x → B − w T = B − x T
38 37 oveq1d ⊢ w = x → B − w T ⁢ T = B − x T ⁢ T
39 34 38 oveq12d ⊢ w = x → w + B − w T ⁢ T = x + B − x T ⁢ T
40 39 cbvmptv ⊢ w ∈ ℝ ⟼ w + B − w T ⁢ T = x ∈ ℝ ⟼ x + B − x T ⁢ T
41 eqeq1 ⊢ w = y → w = B ↔ y = B
42 id ⊢ w = y → w = y
43 41 42 ifbieq2d ⊢ w = y → if w = B A w = if y = B A y
44 43 cbvmptv ⊢ w ∈ A B ⟼ if w = B A w = y ∈ A B ⟼ if y = B A y
45 fveq2 ⊢ z = x → w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ z = w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x
46 45 fveq2d ⊢ z = x → w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ z = w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x
47 46 breq2d ⊢ z = x → Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ z ↔ Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x
48 47 rabbidv ⊢ z = x → j ∈ 0 ..^ M | Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ z = j ∈ 0 ..^ M | Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x
49 fveq2 ⊢ j = i → Q ⁡ j = Q ⁡ i
50 49 breq1d ⊢ j = i → Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x ↔ Q ⁡ i ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x
51 50 cbvrabv ⊢ j ∈ 0 ..^ M | Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x = i ∈ 0 ..^ M | Q ⁡ i ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x
52 48 51 eqtrdi ⊢ z = x → j ∈ 0 ..^ M | Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ z = i ∈ 0 ..^ M | Q ⁡ i ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x
53 52 supeq1d ⊢ z = x → sup j ∈ 0 ..^ M | Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ z ℝ < = sup i ∈ 0 ..^ M | Q ⁡ i ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x ℝ <
54 53 cbvmptv ⊢ z ∈ ℝ ⟼ sup j ∈ 0 ..^ M | Q ⁡ j ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ z ℝ < = x ∈ ℝ ⟼ sup i ∈ 0 ..^ M | Q ⁡ i ≤ w ∈ A B ⟼ if w = B A w ⁡ w ∈ ℝ ⟼ w + B − w T ⁢ T ⁡ x ℝ <
55 1 2 3 4 5 6 7 8 9 10 11 12 13 18 28 33 40 44 54 fourierdlem107 ⊢ φ → ∫ A − X B − X F ⁡ x dx = ∫ A B F ⁡ x dx