Metamath Proof Explorer

Theorem 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 ⊢φ→A∈ℝ
fourierdlem110.b ⊢φ→B∈ℝ
fourierdlem110.t ⊢T=B−A
fourierdlem110.x ⊢φ→X∈ℝ
fourierdlem110.p ⊢P=m∈ℕ⟼p∈ℝ0…m|p⁡0=A∧p⁡m=B∧∀i∈0..^mp⁡i<p⁡i+1
fourierdlem110.m ⊢φ→M∈ℕ
fourierdlem110.q ⊢φ→Q∈P⁡M
fourierdlem110.f ⊢φ→F:ℝ⟶ℂ
fourierdlem110.fper ⊢φ∧x∈ℝ→F⁡x+T=F⁡x
fourierdlem110.fcn ⊢φ∧i∈0..^M→F↾Q⁡iQ⁡i+1:Q⁡iQ⁡i+1⟶cnℂ
fourierdlem110.r ⊢φ∧i∈0..^M→R∈F↾Q⁡iQ⁡i+1limℂQ⁡i
fourierdlem110.l ⊢φ∧i∈0..^M→L∈F↾Q⁡iQ⁡i+1limℂQ⁡i+1
Assertion fourierdlem110 ⊢φ→∫A−XB−XF⁡xdx=∫ABF⁡xdx

Proof

Step Hyp Ref Expression
1 fourierdlem110.a ⊢φ→A∈ℝ
2 fourierdlem110.b ⊢φ→B∈ℝ
3 fourierdlem110.t ⊢T=B−A
4 fourierdlem110.x ⊢φ→X∈ℝ
5 fourierdlem110.p ⊢P=m∈ℕ⟼p∈ℝ0…m|p⁡0=A∧p⁡m=B∧∀i∈0..^mp⁡i<p⁡i+1
6 fourierdlem110.m ⊢φ→M∈ℕ
7 fourierdlem110.q ⊢φ→Q∈P⁡M
8 fourierdlem110.f ⊢φ→F:ℝ⟶ℂ
9 fourierdlem110.fper ⊢φ∧x∈ℝ→F⁡x+T=F⁡x
10 fourierdlem110.fcn ⊢φ∧i∈0..^M→F↾Q⁡iQ⁡i+1:Q⁡iQ⁡i+1⟶cnℂ
11 fourierdlem110.r ⊢φ∧i∈0..^M→R∈F↾Q⁡iQ⁡i+1limℂQ⁡i
12 fourierdlem110.l ⊢φ∧i∈0..^M→L∈F↾Q⁡iQ⁡i+1limℂQ⁡i+1
13 eqid ⊢m∈ℕ⟼p∈ℝ0…m|p⁡0=A−X∧p⁡m=B−X∧∀i∈0..^mp⁡i<p⁡i+1=m∈ℕ⟼p∈ℝ0…m|p⁡0=A−X∧p⁡m=B−X∧∀i∈0..^mp⁡i<p⁡i+1
14 oveq1 ⊢y=x→y+k⁢T=x+k⁢T
15 14 eleq1d ⊢y=x→y+k⁢T∈ran⁡Q↔x+k⁢T∈ran⁡Q
16 15 rexbidv ⊢y=x→∃k∈ℤy+k⁢T∈ran⁡Q↔∃k∈ℤx+k⁢T∈ran⁡Q
17 16 cbvrabv ⊢y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q=x∈A−XB−X|∃k∈ℤx+k⁢T∈ran⁡Q
18 17 uneq2i ⊢A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q=A−XB−X∪x∈A−XB−X|∃k∈ℤx+k⁢T∈ran⁡Q
19 oveq1 ⊢l=k→l⁢T=k⁢T
20 19 oveq2d ⊢l=k→y+l⁢T=y+k⁢T
21 20 eleq1d ⊢l=k→y+l⁢T∈ran⁡Q↔y+k⁢T∈ran⁡Q
22 21 cbvrexvw ⊢∃l∈ℤy+l⁢T∈ran⁡Q↔∃k∈ℤy+k⁢T∈ran⁡Q
23 22 a1i ⊢y∈A−XB−X→∃l∈ℤy+l⁢T∈ran⁡Q↔∃k∈ℤy+k⁢T∈ran⁡Q
24 23 rabbiia ⊢y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q=y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q
25 24 uneq2i ⊢A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q=A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q
26 25 fveq2i ⊢A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q=A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q
27 26 oveq1i ⊢A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1=A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q−1
28 isoeq5 ⊢A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q=A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q→gIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q↔gIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q
29 25 28 ax-mp ⊢gIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q↔gIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q
30 isoeq1 ⊢g=f→gIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q↔fIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q
31 29 30 bitrid ⊢g=f→gIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q↔fIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q
32 31 cbviotavw ⊢ιg|gIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q=ιf|fIsom<,<0…A−XB−X∪y∈A−XB−X|∃l∈ℤy+l⁢T∈ran⁡Q−1A−XB−X∪y∈A−XB−X|∃k∈ℤy+k⁢T∈ran⁡Q
33 id ⊢y=x→y=x
34 oveq2 ⊢y=x→B−y=B−x
35 34 oveq1d ⊢y=x→B−yT=B−xT
36 35 fveq2d ⊢y=x→B−yT=B−xT
37 36 oveq1d ⊢y=x→B−yT⁢T=B−xT⁢T
38 33 37 oveq12d ⊢y=x→y+B−yT⁢T=x+B−xT⁢T
39 38 cbvmptv ⊢y∈ℝ⟼y+B−yT⁢T=x∈ℝ⟼x+B−xT⁢T
40 eqeq1 ⊢y=w→y=B↔w=B
41 id ⊢y=w→y=w
42 40 41 ifbieq2d ⊢y=w→ify=BAy=ifw=BAw
43 42 cbvmptv ⊢y∈AB⟼ify=BAy=w∈AB⟼ifw=BAw
44 fveq2 ⊢z=x→y∈ℝ⟼y+B−yT⁢T⁡z=y∈ℝ⟼y+B−yT⁢T⁡x
45 44 fveq2d ⊢z=x→y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡z=y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡x
46 45 breq2d ⊢z=x→Q⁡j≤y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡z↔Q⁡j≤y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡x
47 46 rabbidv ⊢z=x→j∈0..^M|Q⁡j≤y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡z=j∈0..^M|Q⁡j≤y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡x
48 47 supeq1d ⊢z=x→supj∈0..^M|Q⁡j≤y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡zℝ<=supj∈0..^M|Q⁡j≤y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡xℝ<
49 48 cbvmptv ⊢z∈ℝ⟼supj∈0..^M|Q⁡j≤y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡zℝ<=x∈ℝ⟼supj∈0..^M|Q⁡j≤y∈AB⟼ify=BAy⁡y∈ℝ⟼y+B−yT⁢T⁡xℝ<
50 1 2 3 4 5 6 7 8 9 10 11 12 13 18 27 32 39 43 49 fourierdlem109 ⊢φ→∫A−XB−XF⁡xdx=∫ABF⁡xdx