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 
|- ( ph -> F : CC --> CC )
dvidlem.2 
|- ( ( ph /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )
dvidlem.3 
|- B e. CC
Assertion dvidlem 
|- ( ph -> ( CC _D F ) = ( CC X. { B } ) )

Proof

Step Hyp Ref Expression
1 dvidlem.1 
 |-  ( ph -> F : CC --> CC )
2 dvidlem.2 
 |-  ( ( ph /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )
3 dvidlem.3 
 |-  B e. CC
4 dvfcn 
 |-  ( CC _D F ) : dom ( CC _D F ) --> CC
5 ssidd 
 |-  ( ph -> CC C_ CC )
6 5 1 5 dvbss 
 |-  ( ph -> dom ( CC _D F ) C_ CC )
7 reldv 
 |-  Rel ( CC _D F )
8 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
9 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
10 9 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
11 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
12 11 ntrtop 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) = CC )
13 10 12 ax-mp 
 |-  ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) = CC
14 8 13 eleqtrrdi 
 |-  ( ( ph /\ x e. CC ) -> x e. ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) )
15 limcresi 
 |-  ( ( z e. CC |-> B ) limCC x ) C_ ( ( ( z e. CC |-> B ) |` ( CC \ { x } ) ) limCC x )
16 ssidd 
 |-  ( ( ph /\ x e. CC ) -> CC C_ CC )
17 cncfmptc 
 |-  ( ( B e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( z e. CC |-> B ) e. ( CC -cn-> CC ) )
18 3 16 16 17 mp3an2i 
 |-  ( ( ph /\ x e. CC ) -> ( z e. CC |-> B ) e. ( CC -cn-> CC ) )
19 eqidd 
 |-  ( z = x -> B = B )
20 18 8 19 cnmptlimc 
 |-  ( ( ph /\ x e. CC ) -> B e. ( ( z e. CC |-> B ) limCC x ) )
21 15 20 sseldi 
 |-  ( ( ph /\ x e. CC ) -> B e. ( ( ( z e. CC |-> B ) |` ( CC \ { x } ) ) limCC x ) )
22 eldifsn 
 |-  ( z e. ( CC \ { x } ) <-> ( z e. CC /\ z =/= x ) )
23 2 3exp2 
 |-  ( ph -> ( x e. CC -> ( z e. CC -> ( z =/= x -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B ) ) ) )
24 23 imp43 
 |-  ( ( ( ph /\ x e. CC ) /\ ( z e. CC /\ z =/= x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )
25 22 24 sylan2b 
 |-  ( ( ( ph /\ x e. CC ) /\ z e. ( CC \ { x } ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )
26 25 mpteq2dva 
 |-  ( ( ph /\ x e. CC ) -> ( z e. ( CC \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = ( z e. ( CC \ { x } ) |-> B ) )
27 difss 
 |-  ( CC \ { x } ) C_ CC
28 resmpt 
 |-  ( ( CC \ { x } ) C_ CC -> ( ( z e. CC |-> B ) |` ( CC \ { x } ) ) = ( z e. ( CC \ { x } ) |-> B ) )
29 27 28 ax-mp 
 |-  ( ( z e. CC |-> B ) |` ( CC \ { x } ) ) = ( z e. ( CC \ { x } ) |-> B )
30 26 29 eqtr4di 
 |-  ( ( ph /\ x e. CC ) -> ( z e. ( CC \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = ( ( z e. CC |-> B ) |` ( CC \ { x } ) ) )
31 30 oveq1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( z e. ( CC \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) = ( ( ( z e. CC |-> B ) |` ( CC \ { x } ) ) limCC x ) )
32 21 31 eleqtrrd 
 |-  ( ( ph /\ x e. CC ) -> B e. ( ( z e. ( CC \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) )
33 9 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
34 33 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
35 eqid 
 |-  ( z e. ( CC \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = ( z e. ( CC \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
36 1 adantr 
 |-  ( ( ph /\ x e. CC ) -> F : CC --> CC )
37 34 9 35 16 36 16 eldv 
 |-  ( ( ph /\ x e. CC ) -> ( x ( CC _D F ) B <-> ( x e. ( ( int ` ( TopOpen ` CCfld ) ) ` CC ) /\ B e. ( ( z e. ( CC \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) ) )
38 14 32 37 mpbir2and 
 |-  ( ( ph /\ x e. CC ) -> x ( CC _D F ) B )
39 releldm 
 |-  ( ( Rel ( CC _D F ) /\ x ( CC _D F ) B ) -> x e. dom ( CC _D F ) )
40 7 38 39 sylancr 
 |-  ( ( ph /\ x e. CC ) -> x e. dom ( CC _D F ) )
41 6 40 eqelssd 
 |-  ( ph -> dom ( CC _D F ) = CC )
42 41 feq2d 
 |-  ( ph -> ( ( CC _D F ) : dom ( CC _D F ) --> CC <-> ( CC _D F ) : CC --> CC ) )
43 4 42 mpbii 
 |-  ( ph -> ( CC _D F ) : CC --> CC )
44 43 ffnd 
 |-  ( ph -> ( CC _D F ) Fn CC )
45 fnconstg 
 |-  ( B e. CC -> ( CC X. { B } ) Fn CC )
46 3 45 mp1i 
 |-  ( ph -> ( CC X. { B } ) Fn CC )
47 ffun 
 |-  ( ( CC _D F ) : dom ( CC _D F ) --> CC -> Fun ( CC _D F ) )
48 4 47 mp1i 
 |-  ( ( ph /\ x e. CC ) -> Fun ( CC _D F ) )
49 funbrfvb 
 |-  ( ( Fun ( CC _D F ) /\ x e. dom ( CC _D F ) ) -> ( ( ( CC _D F ) ` x ) = B <-> x ( CC _D F ) B ) )
50 48 40 49 syl2anc 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( CC _D F ) ` x ) = B <-> x ( CC _D F ) B ) )
51 38 50 mpbird 
 |-  ( ( ph /\ x e. CC ) -> ( ( CC _D F ) ` x ) = B )
52 3 a1i 
 |-  ( ph -> B e. CC )
53 fvconst2g 
 |-  ( ( B e. CC /\ x e. CC ) -> ( ( CC X. { B } ) ` x ) = B )
54 52 53 sylan 
 |-  ( ( ph /\ x e. CC ) -> ( ( CC X. { B } ) ` x ) = B )
55 51 54 eqtr4d 
 |-  ( ( ph /\ x e. CC ) -> ( ( CC _D F ) ` x ) = ( ( CC X. { B } ) ` x ) )
56 44 46 55 eqfnfvd 
 |-  ( ph -> ( CC _D F ) = ( CC X. { B } ) )