Metamath Proof Explorer

Theorem dvidlem

Description: Lemma for dvid and dvconst . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses dvidlem.1 ⊢ φ → F : ℂ ⟶ ℂ
dvidlem.2 ⊢ φ ∧ x ∈ ℂ ∧ z ∈ ℂ ∧ z ≠ x → F ⁡ z − F ⁡ x z − x = B
dvidlem.3 ⊢ B ∈ ℂ
Assertion dvidlem ⊢ φ → ℂ D F = ℂ × B

Proof

Step Hyp Ref Expression
1 dvidlem.1 ⊢ φ → F : ℂ ⟶ ℂ
2 dvidlem.2 ⊢ φ ∧ x ∈ ℂ ∧ z ∈ ℂ ∧ z ≠ x → F ⁡ z − F ⁡ x z − x = B
3 dvidlem.3 ⊢ B ∈ ℂ
4 dvfcn ⊢ F ℂ ′ : dom ⁡ F ℂ ′ ⟶ ℂ
5 ssidd ⊢ φ → ℂ ⊆ ℂ
6 5 1 5 dvbss ⊢ φ → dom ⁡ F ℂ ′ ⊆ ℂ
7 reldv ⊢ Rel ⁡ F ℂ ′
8 simpr ⊢ φ ∧ x ∈ ℂ → x ∈ ℂ
9 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
10 9 cnfldtop ⊢ TopOpen ⁡ ℂ fld ∈ Top
11 unicntop ⊢ ℂ = ⋃ TopOpen ⁡ ℂ fld
12 11 ntrtop ⊢ TopOpen ⁡ ℂ fld ∈ Top → int ⁡ TopOpen ⁡ ℂ fld ⁡ ℂ = ℂ
13 10 12 ax-mp ⊢ int ⁡ TopOpen ⁡ ℂ fld ⁡ ℂ = ℂ
14 8 13 eleqtrrdi ⊢ φ ∧ x ∈ ℂ → x ∈ int ⁡ TopOpen ⁡ ℂ fld ⁡ ℂ
15 limcresi ⊢ z ∈ ℂ ⟼ B lim ℂ x ⊆ z ∈ ℂ ⟼ B ↾ ℂ ∖ x lim ℂ x
16 ssidd ⊢ φ ∧ x ∈ ℂ → ℂ ⊆ ℂ
17 cncfmptc ⊢ B ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ → z ∈ ℂ ⟼ B : ℂ ⟶cn ℂ
18 3 16 16 17 mp3an2i ⊢ φ ∧ x ∈ ℂ → z ∈ ℂ ⟼ B : ℂ ⟶cn ℂ
19 eqidd ⊢ z = x → B = B
20 18 8 19 cnmptlimc ⊢ φ ∧ x ∈ ℂ → B ∈ z ∈ ℂ ⟼ B lim ℂ x
21 15 20 sselid ⊢ φ ∧ x ∈ ℂ → B ∈ z ∈ ℂ ⟼ B ↾ ℂ ∖ x lim ℂ x
22 eldifsn ⊢ z ∈ ℂ ∖ x ↔ z ∈ ℂ ∧ z ≠ x
23 2 3exp2 ⊢ φ → x ∈ ℂ → z ∈ ℂ → z ≠ x → F ⁡ z − F ⁡ x z − x = B
24 23 imp43 ⊢ φ ∧ x ∈ ℂ ∧ z ∈ ℂ ∧ z ≠ x → F ⁡ z − F ⁡ x z − x = B
25 22 24 sylan2b ⊢ φ ∧ x ∈ ℂ ∧ z ∈ ℂ ∖ x → F ⁡ z − F ⁡ x z − x = B
26 25 mpteq2dva ⊢ φ ∧ x ∈ ℂ → z ∈ ℂ ∖ x ⟼ F ⁡ z − F ⁡ x z − x = z ∈ ℂ ∖ x ⟼ B
27 difss ⊢ ℂ ∖ x ⊆ ℂ
28 resmpt ⊢ ℂ ∖ x ⊆ ℂ → z ∈ ℂ ⟼ B ↾ ℂ ∖ x = z ∈ ℂ ∖ x ⟼ B
29 27 28 ax-mp ⊢ z ∈ ℂ ⟼ B ↾ ℂ ∖ x = z ∈ ℂ ∖ x ⟼ B
30 26 29 eqtr4di ⊢ φ ∧ x ∈ ℂ → z ∈ ℂ ∖ x ⟼ F ⁡ z − F ⁡ x z − x = z ∈ ℂ ⟼ B ↾ ℂ ∖ x
31 30 oveq1d ⊢ φ ∧ x ∈ ℂ → z ∈ ℂ ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x = z ∈ ℂ ⟼ B ↾ ℂ ∖ x lim ℂ x
32 21 31 eleqtrrd ⊢ φ ∧ x ∈ ℂ → B ∈ z ∈ ℂ ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x
33 9 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
34 33 toponrestid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
35 eqid ⊢ z ∈ ℂ ∖ x ⟼ F ⁡ z − F ⁡ x z − x = z ∈ ℂ ∖ x ⟼ F ⁡ z − F ⁡ x z − x
36 1 adantr ⊢ φ ∧ x ∈ ℂ → F : ℂ ⟶ ℂ
37 34 9 35 16 36 16 eldv ⊢ φ ∧ x ∈ ℂ → x F ℂ ′ B ↔ x ∈ int ⁡ TopOpen ⁡ ℂ fld ⁡ ℂ ∧ B ∈ z ∈ ℂ ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x
38 14 32 37 mpbir2and ⊢ φ ∧ x ∈ ℂ → x F ℂ ′ B
39 releldm ⊢ Rel ⁡ F ℂ ′ ∧ x F ℂ ′ B → x ∈ dom ⁡ F ℂ ′
40 7 38 39 sylancr ⊢ φ ∧ x ∈ ℂ → x ∈ dom ⁡ F ℂ ′
41 6 40 eqelssd ⊢ φ → dom ⁡ F ℂ ′ = ℂ
42 41 feq2d ⊢ φ → F ℂ ′ : dom ⁡ F ℂ ′ ⟶ ℂ ↔ F ℂ ′ : ℂ ⟶ ℂ
43 4 42 mpbii ⊢ φ → F ℂ ′ : ℂ ⟶ ℂ
44 43 ffnd ⊢ φ → F ℂ ′ Fn ℂ
45 fnconstg ⊢ B ∈ ℂ → ℂ × B Fn ℂ
46 3 45 mp1i ⊢ φ → ℂ × B Fn ℂ
47 ffun ⊢ F ℂ ′ : dom ⁡ F ℂ ′ ⟶ ℂ → Fun ⁡ F ℂ ′
48 4 47 mp1i ⊢ φ ∧ x ∈ ℂ → Fun ⁡ F ℂ ′
49 funbrfvb ⊢ Fun ⁡ F ℂ ′ ∧ x ∈ dom ⁡ F ℂ ′ → F ℂ ′ ⁡ x = B ↔ x F ℂ ′ B
50 48 40 49 syl2anc ⊢ φ ∧ x ∈ ℂ → F ℂ ′ ⁡ x = B ↔ x F ℂ ′ B
51 38 50 mpbird ⊢ φ ∧ x ∈ ℂ → F ℂ ′ ⁡ x = B
52 3 a1i ⊢ φ → B ∈ ℂ
53 fvconst2g ⊢ B ∈ ℂ ∧ x ∈ ℂ → ℂ × B ⁡ x = B
54 52 53 sylan ⊢ φ ∧ x ∈ ℂ → ℂ × B ⁡ x = B
55 51 54 eqtr4d ⊢ φ ∧ x ∈ ℂ → F ℂ ′ ⁡ x = ℂ × B ⁡ x
56 44 46 55 eqfnfvd ⊢ φ → ℂ D F = ℂ × B