Metamath Proof Explorer

Theorem itg2const

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

Ref Expression
Assertion itg2const ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝐵 · ( vol ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 reex ⊢ ℝ ∈ V
2 1 a1i ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ℝ ∈ V )
3 simpl3 ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ( 0 [,) +∞ ) )
4 1re ⊢ 1 ∈ ℝ
5 0re ⊢ 0 ∈ ℝ
6 4 5 ifcli ⊢ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ ℝ
7 6 a1i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ ℝ )
8 fconstmpt ⊢ ( ℝ × { 𝐵 } ) = ( 𝑥 ∈ ℝ ↦ 𝐵 )
9 8 a1i ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ℝ × { 𝐵 } ) = ( 𝑥 ∈ ℝ ↦ 𝐵 ) )
10 eqidd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
11 2 3 7 9 10 offval2 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐵 · if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) )
12 ovif2 ⊢ ( 𝐵 · if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( 𝐵 · 1 ) , ( 𝐵 · 0 ) )
13 simp3 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ( 0 [,) +∞ ) )
14 elrege0 ⊢ ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
15 13 14 sylib ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
16 15 simpld ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ℝ )
17 16 recnd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ℂ )
18 17 mulid1d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 · 1 ) = 𝐵 )
19 17 mul01d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 · 0 ) = 0 )
20 18 19 ifeq12d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → if ( 𝑥 ∈ 𝐴 , ( 𝐵 · 1 ) , ( 𝐵 · 0 ) ) = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
21 12 20 syl5eq ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 · if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
22 21 mpteq2dv ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ ( 𝐵 · if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
23 11 22 eqtrd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
24 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
25 24 i1f1 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ dom ∫1 )
26 25 3adant3 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ dom ∫1 )
27 26 16 i1fmulc ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ∈ dom ∫1 )
28 23 27 eqeltrrd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∈ dom ∫1 )
29 15 simprd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝐵 )
30 0le0 ⊢ 0 ≤ 0
31 breq2 ⊢ ( 𝐵 = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) → ( 0 ≤ 𝐵 ↔ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
32 breq2 ⊢ ( 0 = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
33 31 32 ifboth ⊢ ( ( 0 ≤ 𝐵 ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
34 29 30 33 sylancl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
35 34 ralrimivw ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
36 ax-resscn ⊢ ℝ ⊆ ℂ
37 36 a1i ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ℝ ⊆ ℂ )
38 16 adantr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
39 ifcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ )
40 38 5 39 sylancl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ )
41 40 ralrimiva ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ )
42 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
43 42 fnmpt ⊢ ( ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) Fn ℝ )
44 41 43 syl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) Fn ℝ )
45 37 44 0pledm ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
46 5 a1i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
47 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
48 47 a1i ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
49 eqidd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
50 2 46 40 48 49 ofrfval2 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
51 45 50 bitrd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
52 35 51 mpbird ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
53 itg2itg1 ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
54 28 52 53 syl2anc ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
55 26 16 itg1mulc ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫1 ‘ ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ) = ( 𝐵 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ) )
56 23 fveq2d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫1 ‘ ( ( ℝ × { 𝐵 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
57 24 itg11 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( vol ‘ 𝐴 ) )
58 57 3adant3 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) = ( vol ‘ 𝐴 ) )
59 58 oveq2d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) ) = ( 𝐵 · ( vol ‘ 𝐴 ) ) )
60 55 56 59 3eqtr3d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝐵 · ( vol ‘ 𝐴 ) ) )
61 54 60 eqtrd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝐵 · ( vol ‘ 𝐴 ) ) )