Theorem ftc1lem3

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 8-Sep-2015)

	Ref	Expression
Hypotheses	ftc1.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
	ftc1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ftc1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ftc1.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ftc1.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
	ftc1.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	ftc1.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
	ftc1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
	ftc1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
	ftc1.j	⊢ 𝐽 = ( 𝐿 ↾t ℝ )
	ftc1.k	⊢ 𝐾 = ( 𝐿 ↾t 𝐷 )
	ftc1.l	⊢ 𝐿 = ( TopOpen ‘ ℂfld )
Assertion	ftc1lem3	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )

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		ftc1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
9		ftc1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
10		ftc1.j	⊢ 𝐽 = ( 𝐿 ↾t ℝ )
11		ftc1.k	⊢ 𝐾 = ( 𝐿 ↾t 𝐷 )
12		ftc1.l	⊢ 𝐿 = ( TopOpen ‘ ℂfld )
13	12	cnfldtopon	⊢ 𝐿 ∈ ( TopOn ‘ ℂ )
14		ax-resscn	⊢ ℝ ⊆ ℂ
15	6 14	sstrdi	⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
16		resttopon	⊢ ( ( 𝐿 ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐿 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
17	13 15 16	sylancr	⊢ ( 𝜑 → ( 𝐿 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
18	11 17	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝐷 ) )
19	13	a1i	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ℂ ) )
20		cnpf2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐷 ) ∧ 𝐿 ∈ ( TopOn ‘ ℂ ) ∧ 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) ) → 𝐹 : 𝐷 ⟶ ℂ )
21	18 19 9 20	syl3anc	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )