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 ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
dvidlem.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = 𝐵 )
dvidlem.3 ⊢ 𝐵 ∈ ℂ
Assertion dvidlem ( 𝜑 → ( ℂ D 𝐹 ) = ( ℂ × { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 dvidlem.1 ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
2 dvidlem.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = 𝐵 )
3 dvidlem.3 ⊢ 𝐵 ∈ ℂ
4 dvfcn ⊢ ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ
5 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
6 5 1 5 dvbss ⊢ ( 𝜑 → dom ( ℂ D 𝐹 ) ⊆ ℂ )
7 reldv ⊢ Rel ( ℂ D 𝐹 )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℂ ) )
15 limcresi ⊢ ( ( 𝑧 ∈ ℂ ↦ 𝐵 ) limℂ 𝑥 ) ⊆ ( ( ( 𝑧 ∈ ℂ ↦ 𝐵 ) ↾ ( ℂ ∖ { 𝑥 } ) ) limℂ 𝑥 )
16 ssidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ℂ ⊆ ℂ )
17 cncfmptc ⊢ ( ( 𝐵 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ ℂ ↦ 𝐵 ) ∈ ( ℂ –cn→ ℂ ) )
18 3 16 16 17 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑧 ∈ ℂ ↦ 𝐵 ) ∈ ( ℂ –cn→ ℂ ) )
19 eqidd ⊢ ( 𝑧 = 𝑥 → 𝐵 = 𝐵 )
20 18 8 19 cnmptlimc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ( ( 𝑧 ∈ ℂ ↦ 𝐵 ) limℂ 𝑥 ) )
21 15 20 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ( ( ( 𝑧 ∈ ℂ ↦ 𝐵 ) ↾ ( ℂ ∖ { 𝑥 } ) ) limℂ 𝑥 ) )
22 eldifsn ⊢ ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↔ ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) )
23 2 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ → ( 𝑧 ∈ ℂ → ( 𝑧 ≠ 𝑥 → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = 𝐵 ) ) ) )
24 23 imp43 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 𝑥 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = 𝐵 )
25 22 24 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = 𝐵 )
26 25 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ 𝐵 ) )
27 difss ⊢ ( ℂ ∖ { 𝑥 } ) ⊆ ℂ
28 resmpt ⊢ ( ( ℂ ∖ { 𝑥 } ) ⊆ ℂ → ( ( 𝑧 ∈ ℂ ↦ 𝐵 ) ↾ ( ℂ ∖ { 𝑥 } ) ) = ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ 𝐵 ) )
29 27 28 ax-mp ⊢ ( ( 𝑧 ∈ ℂ ↦ 𝐵 ) ↾ ( ℂ ∖ { 𝑥 } ) ) = ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ 𝐵 )
30 26 29 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( ( 𝑧 ∈ ℂ ↦ 𝐵 ) ↾ ( ℂ ∖ { 𝑥 } ) ) )
31 30 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) = ( ( ( 𝑧 ∈ ℂ ↦ 𝐵 ) ↾ ( ℂ ∖ { 𝑥 } ) ) limℂ 𝑥 ) )
32 21 31 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ( ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
33 9 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
34 33 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
35 eqid ⊢ ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
36 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐹 : ℂ ⟶ ℂ )
37 34 9 35 16 36 16 eldv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ( ℂ D 𝐹 ) 𝐵 ↔ ( 𝑥 ∈ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℂ ) ∧ 𝐵 ∈ ( ( 𝑧 ∈ ( ℂ ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ) )
38 14 32 37 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ( ℂ D 𝐹 ) 𝐵 )
39 releldm ⊢ ( ( Rel ( ℂ D 𝐹 ) ∧ 𝑥 ( ℂ D 𝐹 ) 𝐵 ) → 𝑥 ∈ dom ( ℂ D 𝐹 ) )
40 7 38 39 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ dom ( ℂ D 𝐹 ) )
41 6 40 eqelssd ⊢ ( 𝜑 → dom ( ℂ D 𝐹 ) = ℂ )
42 41 feq2d ⊢ ( 𝜑 → ( ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ ↔ ( ℂ D 𝐹 ) : ℂ ⟶ ℂ ) )
43 4 42 mpbii ⊢ ( 𝜑 → ( ℂ D 𝐹 ) : ℂ ⟶ ℂ )
44 43 ffnd ⊢ ( 𝜑 → ( ℂ D 𝐹 ) Fn ℂ )
45 fnconstg ⊢ ( 𝐵 ∈ ℂ → ( ℂ × { 𝐵 } ) Fn ℂ )
46 3 45 mp1i ⊢ ( 𝜑 → ( ℂ × { 𝐵 } ) Fn ℂ )
47 ffun ⊢ ( ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ → Fun ( ℂ D 𝐹 ) )
48 4 47 mp1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Fun ( ℂ D 𝐹 ) )
49 funbrfvb ⊢ ( ( Fun ( ℂ D 𝐹 ) ∧ 𝑥 ∈ dom ( ℂ D 𝐹 ) ) → ( ( ( ℂ D 𝐹 ) ‘ 𝑥 ) = 𝐵 ↔ 𝑥 ( ℂ D 𝐹 ) 𝐵 ) )
50 48 40 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( ℂ D 𝐹 ) ‘ 𝑥 ) = 𝐵 ↔ 𝑥 ( ℂ D 𝐹 ) 𝐵 ) )
51 38 50 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ℂ D 𝐹 ) ‘ 𝑥 ) = 𝐵 )
52 3 a1i ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
53 fvconst2g ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( ℂ × { 𝐵 } ) ‘ 𝑥 ) = 𝐵 )
54 52 53 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ℂ × { 𝐵 } ) ‘ 𝑥 ) = 𝐵 )
55 51 54 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ℂ D 𝐹 ) ‘ 𝑥 ) = ( ( ℂ × { 𝐵 } ) ‘ 𝑥 ) )
56 44 46 55 eqfnfvd ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( ℂ × { 𝐵 } ) )