Theorem itgmulc2nclem1

Description: Lemma for itgmulc2nc ; cf. itgmulc2lem1 . (Contributed by Brendan Leahy, 17-Nov-2017)

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

Proof

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