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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )