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 𝑥 )