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..^mp⁡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⁡iQ⁡i+1:Q⁡iQ⁡i+1⟶cnℂ
fourierdlem108.r ⊢φ∧i∈0..^M→R∈F↾Q⁡iQ⁡i+1limℂQ⁡i
fourierdlem108.l ⊢φ∧i∈0..^M→L∈F↾Q⁡iQ⁡i+1limℂQ⁡i+1
Assertion fourierdlem108 ⊢φ→∫A−XB−XF⁡xdx=∫ABF⁡xdx

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..^mp⁡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⁡iQ⁡i+1:Q⁡iQ⁡i+1⟶cnℂ
11 fourierdlem108.r ⊢φ∧i∈0..^M→R∈F↾Q⁡iQ⁡i+1limℂQ⁡i
12 fourierdlem108.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=A∧∀i∈0..^mp⁡i<p⁡i+1=m∈ℕ⟼p∈ℝ0…m|p⁡0=A−X∧p⁡m=A∧∀i∈0..^mp⁡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−XA|∃k∈ℤw+k⁢T∈ran⁡Q=y∈A−XA|∃k∈ℤy+k⁢T∈ran⁡Q
18 17 uneq2i ⊢A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q=A−XA∪y∈A−XA|∃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−XA∃l∈ℤw+l⁢T∈ran⁡Q↔∃k∈ℤw+k⁢T∈ran⁡Q
24 rabbi ⊢∀w∈A−XA∃l∈ℤw+l⁢T∈ran⁡Q↔∃k∈ℤw+k⁢T∈ran⁡Q↔w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q=w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q
25 23 24 mpbi ⊢w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q=w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q
26 25 uneq2i ⊢A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q=A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q
27 26 fveq2i ⊢A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q=A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q
28 27 oveq1i ⊢A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1=A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q−1
29 isoeq5 ⊢A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q=A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q→gIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q↔gIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q
30 26 29 ax-mp ⊢gIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q↔gIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q
31 isoeq1 ⊢g=f→gIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q↔fIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q
32 30 31 bitrid ⊢g=f→gIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q↔fIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃k∈ℤw+k⁢T∈ran⁡Q
33 32 cbviotavw ⊢ιg|gIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q=ιf|fIsom<,<0…A−XA∪w∈A−XA|∃l∈ℤw+l⁢T∈ran⁡Q−1A−XA∪w∈A−XA|∃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−wT=B−xT
37 36 fveq2d ⊢w=x→B−wT=B−xT
38 37 oveq1d ⊢w=x→B−wT⁢T=B−xT⁢T
39 34 38 oveq12d ⊢w=x→w+B−wT⁢T=x+B−xT⁢T
40 39 cbvmptv ⊢w∈ℝ⟼w+B−wT⁢T=x∈ℝ⟼x+B−xT⁢T
41 eqeq1 ⊢w=y→w=B↔y=B
42 id ⊢w=y→w=y
43 41 42 ifbieq2d ⊢w=y→ifw=BAw=ify=BAy
44 43 cbvmptv ⊢w∈AB⟼ifw=BAw=y∈AB⟼ify=BAy
45 fveq2 ⊢z=x→w∈ℝ⟼w+B−wT⁢T⁡z=w∈ℝ⟼w+B−wT⁢T⁡x
46 45 fveq2d ⊢z=x→w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡z=w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
47 46 breq2d ⊢z=x→Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡z↔Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
48 47 rabbidv ⊢z=x→j∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡z=j∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
49 fveq2 ⊢j=i→Q⁡j=Q⁡i
50 49 breq1d ⊢j=i→Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x↔Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
51 50 cbvrabv ⊢j∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x=i∈0..^M|Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
52 48 51 eqtrdi ⊢z=x→j∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡z=i∈0..^M|Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
53 52 supeq1d ⊢z=x→supj∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡zℝ<=supi∈0..^M|Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡xℝ<
54 53 cbvmptv ⊢z∈ℝ⟼supj∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡zℝ<=x∈ℝ⟼supi∈0..^M|Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡xℝ<
55 1 2 3 4 5 6 7 8 9 10 11 12 13 18 28 33 40 44 54 fourierdlem107 ⊢φ→∫A−XB−XF⁡xdx=∫ABF⁡xdx