This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgmulc2lem1

Description: Lemma for itgmulc2 : positive real case. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
itgmulc2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgmulc2.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
itgmulc2.4 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
itgmulc2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
itgmulc2.6 ⊢ ( 𝜑 → 0 ≤ 𝐶 )
itgmulc2.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
Assertion itgmulc2lem1 ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgmulc2.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 itgmulc2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 itgmulc2.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
4 itgmulc2.4 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5 itgmulc2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
6 itgmulc2.6 ⊢ ( 𝜑 → 0 ≤ 𝐶 )
7 itgmulc2.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
8 elrege0 ⊢ ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
9 5 7 8 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
10 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
11 10 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
12 9 11 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
14 13 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
15 5 7 iblpos ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ∈ ℝ ) ) )
16 3 15 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ∈ ℝ ) )
17 16 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ∈ ℝ )
18 elrege0 ⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
19 4 6 18 sylanbrc ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
20 14 17 19 itg2mulc ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { 𝐶 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ) = ( 𝐶 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ) )
21 reex ⊢ ℝ ∈ V
22 21 a1i ⊢ ( 𝜑 → ℝ ∈ V )
23 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐶 ∈ ℝ )
24 fconstmpt ⊢ ( ℝ × { 𝐶 } ) = ( 𝑥 ∈ ℝ ↦ 𝐶 )
25 24 a1i ⊢ ( 𝜑 → ( ℝ × { 𝐶 } ) = ( 𝑥 ∈ ℝ ↦ 𝐶 ) )
26 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) )
27 22 23 13 25 26 offval2 ⊢ ( 𝜑 → ( ( ℝ × { 𝐶 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐶 · if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
28 ovif2 ⊢ ( 𝐶 · if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , ( 𝐶 · 0 ) )
29 1 mul01d ⊢ ( 𝜑 → ( 𝐶 · 0 ) = 0 )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐶 · 0 ) = 0 )
31 30 ifeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , ( 𝐶 · 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , 0 ) )
32 28 31 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐶 · if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , 0 ) )
33 32 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( 𝐶 · if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , 0 ) ) )
34 27 33 eqtrd ⊢ ( 𝜑 → ( ( ℝ × { 𝐶 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , 0 ) ) )
35 34 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { 𝐶 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , 0 ) ) ) )
36 20 35 eqtr3d ⊢ ( 𝜑 → ( 𝐶 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , 0 ) ) ) )
37 5 3 7 itgposval ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
38 37 oveq2d ⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ( 𝐶 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) ) )
39 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
40 39 5 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℝ )
41 1 2 3 iblmulc2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 )
42 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐶 )
43 39 5 42 7 mulge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( 𝐶 · 𝐵 ) )
44 40 41 43 itgposval ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐶 · 𝐵 ) , 0 ) ) ) )
45 36 38 44 3eqtr4d ⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )