Theorem ftc1lem2

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 12-Aug-2014)

	Ref	Expression
Hypotheses	ftc1.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
	ftc1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ftc1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ftc1.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ftc1.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
	ftc1.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	ftc1.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
	ftc1a.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
Assertion	ftc1lem2	⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		ftc1.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2		ftc1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3		ftc1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		ftc1.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5		ftc1.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6		ftc1.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7		ftc1.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8		ftc1a.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
9		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑥 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
10	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
11	10	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ* )
12		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
13	2 3 12	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
14	13	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
15	14	simp3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
16		iooss2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) → ( 𝐴 (,) 𝑥 ) ⊆ ( 𝐴 (,) 𝐵 ) )
17	11 15 16	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑥 ) ⊆ ( 𝐴 (,) 𝐵 ) )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
19	17 18	sstrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑥 ) ⊆ 𝐷 )
20		ioombl	⊢ ( 𝐴 (,) 𝑥 ) ∈ dom vol
21	20	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑥 ) ∈ dom vol )
22		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
23	8	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
24	23 7	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
26	19 21 22 25	iblss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑥 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
27	9 26	itgcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ )
28	27 1	fmptd	⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )