Metamath Proof Explorer

Theorem itgitg1

Description: Transfer an integral using S.1 to an equivalent integral using S. . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion itgitg1 ⊢F∈dom⁡∫1→∫ℝF⁡xdx=∫1⁡F

Proof

Step Hyp Ref Expression
1 i1ff ⊢F∈dom⁡∫1→F:ℝ⟶ℝ
2 1 ffvelcdmda ⊢F∈dom⁡∫1∧x∈ℝ→F⁡x∈ℝ
3 1 feqmptd ⊢F∈dom⁡∫1→F=x∈ℝ⟼F⁡x
4 i1fibl ⊢F∈dom⁡∫1→F∈𝐿1
5 3 4 eqeltrrd ⊢F∈dom⁡∫1→x∈ℝ⟼F⁡x∈𝐿1
6 2 5 itgreval ⊢F∈dom⁡∫1→∫ℝF⁡xdx=∫ℝif0≤F⁡xF⁡x0dx−∫ℝif0≤−F⁡x−F⁡x0dx
7 0re ⊢0∈ℝ
8 ifcl ⊢F⁡x∈ℝ∧0∈ℝ→if0≤F⁡xF⁡x0∈ℝ
9 2 7 8 sylancl ⊢F∈dom⁡∫1∧x∈ℝ→if0≤F⁡xF⁡x0∈ℝ
10 max1 ⊢0∈ℝ∧F⁡x∈ℝ→0≤if0≤F⁡xF⁡x0
11 7 2 10 sylancr ⊢F∈dom⁡∫1∧x∈ℝ→0≤if0≤F⁡xF⁡x0
12 id ⊢F∈dom⁡∫1→F∈dom⁡∫1
13 3 12 eqeltrrd ⊢F∈dom⁡∫1→x∈ℝ⟼F⁡x∈dom⁡∫1
14 13 i1fposd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0∈dom⁡∫1
15 i1fibl ⊢x∈ℝ⟼if0≤F⁡xF⁡x0∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0∈𝐿1
16 14 15 syl ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0∈𝐿1
17 9 11 16 itgitg2 ⊢F∈dom⁡∫1→∫ℝif0≤F⁡xF⁡x0dx=∫2⁡x∈ℝ⟼if0≤F⁡xF⁡x0
18 11 ralrimiva ⊢F∈dom⁡∫1→∀x∈ℝ0≤if0≤F⁡xF⁡x0
19 reex ⊢ℝ∈V
20 19 a1i ⊢F∈dom⁡∫1→ℝ∈V
21 7 a1i ⊢F∈dom⁡∫1∧x∈ℝ→0∈ℝ
22 fconstmpt ⊢ℝ×0=x∈ℝ⟼0
23 22 a1i ⊢F∈dom⁡∫1→ℝ×0=x∈ℝ⟼0
24 eqidd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0=x∈ℝ⟼if0≤F⁡xF⁡x0
25 20 21 9 23 24 ofrfval2 ⊢F∈dom⁡∫1→ℝ×0≤fx∈ℝ⟼if0≤F⁡xF⁡x0↔∀x∈ℝ0≤if0≤F⁡xF⁡x0
26 18 25 mpbird ⊢F∈dom⁡∫1→ℝ×0≤fx∈ℝ⟼if0≤F⁡xF⁡x0
27 ax-resscn ⊢ℝ⊆ℂ
28 27 a1i ⊢F∈dom⁡∫1→ℝ⊆ℂ
29 9 fmpttd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0:ℝ⟶ℝ
30 29 ffnd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0Fnℝ
31 28 30 0pledm ⊢F∈dom⁡∫1→0𝑝≤fx∈ℝ⟼if0≤F⁡xF⁡x0↔ℝ×0≤fx∈ℝ⟼if0≤F⁡xF⁡x0
32 26 31 mpbird ⊢F∈dom⁡∫1→0𝑝≤fx∈ℝ⟼if0≤F⁡xF⁡x0
33 itg2itg1 ⊢x∈ℝ⟼if0≤F⁡xF⁡x0∈dom⁡∫1∧0𝑝≤fx∈ℝ⟼if0≤F⁡xF⁡x0→∫2⁡x∈ℝ⟼if0≤F⁡xF⁡x0=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0
34 14 32 33 syl2anc ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼if0≤F⁡xF⁡x0=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0
35 17 34 eqtrd ⊢F∈dom⁡∫1→∫ℝif0≤F⁡xF⁡x0dx=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0
36 2 renegcld ⊢F∈dom⁡∫1∧x∈ℝ→−F⁡x∈ℝ
37 ifcl ⊢−F⁡x∈ℝ∧0∈ℝ→if0≤−F⁡x−F⁡x0∈ℝ
38 36 7 37 sylancl ⊢F∈dom⁡∫1∧x∈ℝ→if0≤−F⁡x−F⁡x0∈ℝ
39 max1 ⊢0∈ℝ∧−F⁡x∈ℝ→0≤if0≤−F⁡x−F⁡x0
40 7 36 39 sylancr ⊢F∈dom⁡∫1∧x∈ℝ→0≤if0≤−F⁡x−F⁡x0
41 neg1rr ⊢−1∈ℝ
42 41 a1i ⊢F∈dom⁡∫1∧x∈ℝ→−1∈ℝ
43 fconstmpt ⊢ℝ×−1=x∈ℝ⟼−1
44 43 a1i ⊢F∈dom⁡∫1→ℝ×−1=x∈ℝ⟼−1
45 20 42 2 44 3 offval2 ⊢F∈dom⁡∫1→ℝ×−1×fF=x∈ℝ⟼-1⁢F⁡x
46 2 recnd ⊢F∈dom⁡∫1∧x∈ℝ→F⁡x∈ℂ
47 46 mulm1d ⊢F∈dom⁡∫1∧x∈ℝ→-1⁢F⁡x=−F⁡x
48 47 mpteq2dva ⊢F∈dom⁡∫1→x∈ℝ⟼-1⁢F⁡x=x∈ℝ⟼−F⁡x
49 45 48 eqtrd ⊢F∈dom⁡∫1→ℝ×−1×fF=x∈ℝ⟼−F⁡x
50 41 a1i ⊢F∈dom⁡∫1→−1∈ℝ
51 12 50 i1fmulc ⊢F∈dom⁡∫1→ℝ×−1×fF∈dom⁡∫1
52 49 51 eqeltrrd ⊢F∈dom⁡∫1→x∈ℝ⟼−F⁡x∈dom⁡∫1
53 52 i1fposd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0∈dom⁡∫1
54 i1fibl ⊢x∈ℝ⟼if0≤−F⁡x−F⁡x0∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0∈𝐿1
55 53 54 syl ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0∈𝐿1
56 38 40 55 itgitg2 ⊢F∈dom⁡∫1→∫ℝif0≤−F⁡x−F⁡x0dx=∫2⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
57 40 ralrimiva ⊢F∈dom⁡∫1→∀x∈ℝ0≤if0≤−F⁡x−F⁡x0
58 eqidd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0=x∈ℝ⟼if0≤−F⁡x−F⁡x0
59 20 21 38 23 58 ofrfval2 ⊢F∈dom⁡∫1→ℝ×0≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0↔∀x∈ℝ0≤if0≤−F⁡x−F⁡x0
60 57 59 mpbird ⊢F∈dom⁡∫1→ℝ×0≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0
61 38 fmpttd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0:ℝ⟶ℝ
62 61 ffnd ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤−F⁡x−F⁡x0Fnℝ
63 28 62 0pledm ⊢F∈dom⁡∫1→0𝑝≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0↔ℝ×0≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0
64 60 63 mpbird ⊢F∈dom⁡∫1→0𝑝≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0
65 itg2itg1 ⊢x∈ℝ⟼if0≤−F⁡x−F⁡x0∈dom⁡∫1∧0𝑝≤fx∈ℝ⟼if0≤−F⁡x−F⁡x0→∫2⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0=∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
66 53 64 65 syl2anc ⊢F∈dom⁡∫1→∫2⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0=∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
67 56 66 eqtrd ⊢F∈dom⁡∫1→∫ℝif0≤−F⁡x−F⁡x0dx=∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
68 35 67 oveq12d ⊢F∈dom⁡∫1→∫ℝif0≤F⁡xF⁡x0dx−∫ℝif0≤−F⁡x−F⁡x0dx=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0−∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
69 itg1sub ⊢x∈ℝ⟼if0≤F⁡xF⁡x0∈dom⁡∫1∧x∈ℝ⟼if0≤−F⁡x−F⁡x0∈dom⁡∫1→∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0−fx∈ℝ⟼if0≤−F⁡x−F⁡x0=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0−∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
70 14 53 69 syl2anc ⊢F∈dom⁡∫1→∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0−fx∈ℝ⟼if0≤−F⁡x−F⁡x0=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0−∫1⁡x∈ℝ⟼if0≤−F⁡x−F⁡x0
71 68 70 eqtr4d ⊢F∈dom⁡∫1→∫ℝif0≤F⁡xF⁡x0dx−∫ℝif0≤−F⁡x−F⁡x0dx=∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0−fx∈ℝ⟼if0≤−F⁡x−F⁡x0
72 max0sub ⊢F⁡x∈ℝ→if0≤F⁡xF⁡x0−if0≤−F⁡x−F⁡x0=F⁡x
73 2 72 syl ⊢F∈dom⁡∫1∧x∈ℝ→if0≤F⁡xF⁡x0−if0≤−F⁡x−F⁡x0=F⁡x
74 73 mpteq2dva ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0−if0≤−F⁡x−F⁡x0=x∈ℝ⟼F⁡x
75 20 9 38 24 58 offval2 ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0−fx∈ℝ⟼if0≤−F⁡x−F⁡x0=x∈ℝ⟼if0≤F⁡xF⁡x0−if0≤−F⁡x−F⁡x0
76 74 75 3 3eqtr4d ⊢F∈dom⁡∫1→x∈ℝ⟼if0≤F⁡xF⁡x0−fx∈ℝ⟼if0≤−F⁡x−F⁡x0=F
77 76 fveq2d ⊢F∈dom⁡∫1→∫1⁡x∈ℝ⟼if0≤F⁡xF⁡x0−fx∈ℝ⟼if0≤−F⁡x−F⁡x0=∫1⁡F
78 6 71 77 3eqtrd ⊢F∈dom⁡∫1→∫ℝF⁡xdx=∫1⁡F