Metamath Proof Explorer

Theorem itgconst

Description: Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Assertion itgconst ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→∫ABdx=B⁢vol⁡A

Proof

Step Hyp Ref Expression
1 simpl ⊢y=ℜ⁡B∧x∈A→y=ℜ⁡B
2 1 itgeq2dv ⊢y=ℜ⁡B→∫Aydx=∫Aℜ⁡Bdx
3 oveq1 ⊢y=ℜ⁡B→y⁢vol⁡A=ℜ⁡B⁢vol⁡A
4 2 3 eqeq12d ⊢y=ℜ⁡B→∫Aydx=y⁢vol⁡A↔∫Aℜ⁡Bdx=ℜ⁡B⁢vol⁡A
5 simplr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ∧x∈A→y∈ℝ
6 fconstmpt ⊢A×y=x∈A⟼y
7 simpl1 ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→A∈dom⁡vol
8 simp2 ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→vol⁡A∈ℝ
9 8 adantr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→vol⁡A∈ℝ
10 simpr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→y∈ℝ
11 10 recnd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→y∈ℂ
12 iblconst ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧y∈ℂ→A×y∈𝐿1
13 7 9 11 12 syl3anc ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→A×y∈𝐿1
14 6 13 eqeltrrid ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→x∈A⟼y∈𝐿1
15 5 14 itgrevallem1 ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→∫Aydx=∫2⁡x∈ℝ⟼ifx∈A∧0≤yy0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−y−y0
16 ifan ⊢ifx∈A∧0≤yy0=ifx∈Aif0≤yy00
17 16 mpteq2i ⊢x∈ℝ⟼ifx∈A∧0≤yy0=x∈ℝ⟼ifx∈Aif0≤yy00
18 17 fveq2i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤yy0=∫2⁡x∈ℝ⟼ifx∈Aif0≤yy00
19 0re ⊢0∈ℝ
20 ifcl ⊢y∈ℝ∧0∈ℝ→if0≤yy0∈ℝ
21 10 19 20 sylancl ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤yy0∈ℝ
22 max1 ⊢0∈ℝ∧y∈ℝ→0≤if0≤yy0
23 19 10 22 sylancr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→0≤if0≤yy0
24 elrege0 ⊢if0≤yy0∈0+∞↔if0≤yy0∈ℝ∧0≤if0≤yy0
25 21 23 24 sylanbrc ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤yy0∈0+∞
26 itg2const ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧if0≤yy0∈0+∞→∫2⁡x∈ℝ⟼ifx∈Aif0≤yy00=if0≤yy0⁢vol⁡A
27 7 9 25 26 syl3anc ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→∫2⁡x∈ℝ⟼ifx∈Aif0≤yy00=if0≤yy0⁢vol⁡A
28 18 27 eqtrid ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→∫2⁡x∈ℝ⟼ifx∈A∧0≤yy0=if0≤yy0⁢vol⁡A
29 ifan ⊢ifx∈A∧0≤−y−y0=ifx∈Aif0≤−y−y00
30 29 mpteq2i ⊢x∈ℝ⟼ifx∈A∧0≤−y−y0=x∈ℝ⟼ifx∈Aif0≤−y−y00
31 30 fveq2i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−y−y0=∫2⁡x∈ℝ⟼ifx∈Aif0≤−y−y00
32 renegcl ⊢y∈ℝ→−y∈ℝ
33 32 adantl ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→−y∈ℝ
34 ifcl ⊢−y∈ℝ∧0∈ℝ→if0≤−y−y0∈ℝ
35 33 19 34 sylancl ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤−y−y0∈ℝ
36 max1 ⊢0∈ℝ∧−y∈ℝ→0≤if0≤−y−y0
37 19 33 36 sylancr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→0≤if0≤−y−y0
38 elrege0 ⊢if0≤−y−y0∈0+∞↔if0≤−y−y0∈ℝ∧0≤if0≤−y−y0
39 35 37 38 sylanbrc ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤−y−y0∈0+∞
40 itg2const ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧if0≤−y−y0∈0+∞→∫2⁡x∈ℝ⟼ifx∈Aif0≤−y−y00=if0≤−y−y0⁢vol⁡A
41 7 9 39 40 syl3anc ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→∫2⁡x∈ℝ⟼ifx∈Aif0≤−y−y00=if0≤−y−y0⁢vol⁡A
42 31 41 eqtrid ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−y−y0=if0≤−y−y0⁢vol⁡A
43 28 42 oveq12d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→∫2⁡x∈ℝ⟼ifx∈A∧0≤yy0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−y−y0=if0≤yy0⁢vol⁡A−if0≤−y−y0⁢vol⁡A
44 21 recnd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤yy0∈ℂ
45 35 recnd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤−y−y0∈ℂ
46 8 recnd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→vol⁡A∈ℂ
47 46 adantr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→vol⁡A∈ℂ
48 44 45 47 subdird ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤yy0−if0≤−y−y0⁢vol⁡A=if0≤yy0⁢vol⁡A−if0≤−y−y0⁢vol⁡A
49 max0sub ⊢y∈ℝ→if0≤yy0−if0≤−y−y0=y
50 49 adantl ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤yy0−if0≤−y−y0=y
51 50 oveq1d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→if0≤yy0−if0≤−y−y0⁢vol⁡A=y⁢vol⁡A
52 43 48 51 3eqtr2rd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→y⁢vol⁡A=∫2⁡x∈ℝ⟼ifx∈A∧0≤yy0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−y−y0
53 15 52 eqtr4d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧y∈ℝ→∫Aydx=y⁢vol⁡A
54 53 ralrimiva ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→∀y∈ℝ∫Aydx=y⁢vol⁡A
55 recl ⊢B∈ℂ→ℜ⁡B∈ℝ
56 55 3ad2ant3 ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→ℜ⁡B∈ℝ
57 4 54 56 rspcdva ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→∫Aℜ⁡Bdx=ℜ⁡B⁢vol⁡A
58 simpl ⊢y=ℑ⁡B∧x∈A→y=ℑ⁡B
59 58 itgeq2dv ⊢y=ℑ⁡B→∫Aydx=∫Aℑ⁡Bdx
60 oveq1 ⊢y=ℑ⁡B→y⁢vol⁡A=ℑ⁡B⁢vol⁡A
61 59 60 eqeq12d ⊢y=ℑ⁡B→∫Aydx=y⁢vol⁡A↔∫Aℑ⁡Bdx=ℑ⁡B⁢vol⁡A
62 imcl ⊢B∈ℂ→ℑ⁡B∈ℝ
63 62 3ad2ant3 ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→ℑ⁡B∈ℝ
64 61 54 63 rspcdva ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→∫Aℑ⁡Bdx=ℑ⁡B⁢vol⁡A
65 64 oveq2d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→i⁢∫Aℑ⁡Bdx=i⁢ℑ⁡B⁢vol⁡A
66 ax-icn ⊢i∈ℂ
67 66 a1i ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→i∈ℂ
68 63 recnd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→ℑ⁡B∈ℂ
69 67 68 46 mulassd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→i⁢ℑ⁡B⁢vol⁡A=i⁢ℑ⁡B⁢vol⁡A
70 65 69 eqtr4d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→i⁢∫Aℑ⁡Bdx=i⁢ℑ⁡B⁢vol⁡A
71 57 70 oveq12d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx=ℜ⁡B⁢vol⁡A+i⁢ℑ⁡B⁢vol⁡A
72 56 recnd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→ℜ⁡B∈ℂ
73 mulcl ⊢i∈ℂ∧ℑ⁡B∈ℂ→i⁢ℑ⁡B∈ℂ
74 66 68 73 sylancr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→i⁢ℑ⁡B∈ℂ
75 72 74 46 adddird ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→ℜ⁡B+i⁢ℑ⁡B⁢vol⁡A=ℜ⁡B⁢vol⁡A+i⁢ℑ⁡B⁢vol⁡A
76 71 75 eqtr4d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx=ℜ⁡B+i⁢ℑ⁡B⁢vol⁡A
77 simpl3 ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ∧x∈A→B∈ℂ
78 fconstmpt ⊢A×B=x∈A⟼B
79 iblconst ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→A×B∈𝐿1
80 78 79 eqeltrrid ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→x∈A⟼B∈𝐿1
81 77 80 itgcnval ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→∫ABdx=∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx
82 replim ⊢B∈ℂ→B=ℜ⁡B+i⁢ℑ⁡B
83 82 3ad2ant3 ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→B=ℜ⁡B+i⁢ℑ⁡B
84 83 oveq1d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→B⁢vol⁡A=ℜ⁡B+i⁢ℑ⁡B⁢vol⁡A
85 76 81 84 3eqtr4d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧B∈ℂ→∫ABdx=B⁢vol⁡A