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 ⊢ G = x ∈ A B ⟼ ∫ A x F ⁡ t dt
ftc1.a ⊢ φ → A ∈ ℝ
ftc1.b ⊢ φ → B ∈ ℝ
ftc1.le ⊢ φ → A ≤ B
ftc1.s ⊢ φ → A B ⊆ D
ftc1.d ⊢ φ → D ⊆ ℝ
ftc1.i ⊢ φ → F ∈ 𝐿 1
ftc1.c ⊢ φ → C ∈ A B
ftc1.f ⊢ φ → F ∈ K CnP L ⁡ C
ftc1.j ⊢ J = L ↾ 𝑡 ℝ
ftc1.k ⊢ K = L ↾ 𝑡 D
ftc1.l ⊢ L = TopOpen ⁡ ℂ fld
Assertion ftc1lem3 ⊢ φ → F : D ⟶ ℂ

Proof

Step Hyp Ref Expression
1 ftc1.g ⊢ G = x ∈ A B ⟼ ∫ A x F ⁡ t dt
2 ftc1.a ⊢ φ → A ∈ ℝ
3 ftc1.b ⊢ φ → B ∈ ℝ
4 ftc1.le ⊢ φ → A ≤ B
5 ftc1.s ⊢ φ → A B ⊆ D
6 ftc1.d ⊢ φ → D ⊆ ℝ
7 ftc1.i ⊢ φ → F ∈ 𝐿 1
8 ftc1.c ⊢ φ → C ∈ A B
9 ftc1.f ⊢ φ → F ∈ K CnP L ⁡ C
10 ftc1.j ⊢ J = L ↾ 𝑡 ℝ
11 ftc1.k ⊢ K = L ↾ 𝑡 D
12 ftc1.l ⊢ L = TopOpen ⁡ ℂ fld
13 12 cnfldtopon ⊢ L ∈ TopOn ⁡ ℂ
14 ax-resscn ⊢ ℝ ⊆ ℂ
15 6 14 sstrdi ⊢ φ → D ⊆ ℂ
16 resttopon ⊢ L ∈ TopOn ⁡ ℂ ∧ D ⊆ ℂ → L ↾ 𝑡 D ∈ TopOn ⁡ D
17 13 15 16 sylancr ⊢ φ → L ↾ 𝑡 D ∈ TopOn ⁡ D
18 11 17 eqeltrid ⊢ φ → K ∈ TopOn ⁡ D
19 13 a1i ⊢ φ → L ∈ TopOn ⁡ ℂ
20 cnpf2 ⊢ K ∈ TopOn ⁡ D ∧ L ∈ TopOn ⁡ ℂ ∧ F ∈ K CnP L ⁡ C → F : D ⟶ ℂ
21 18 19 9 20 syl3anc ⊢ φ → F : D ⟶ ℂ