Metamath Proof Explorer

Theorem dvcobr

Description: The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses dvco.f 
|- ( ph -> F : X --> CC )
dvco.x 
|- ( ph -> X C_ S )
dvco.g 
|- ( ph -> G : Y --> X )
dvco.y 
|- ( ph -> Y C_ T )
dvcobr.s 
|- ( ph -> S C_ CC )
dvcobr.t 
|- ( ph -> T C_ CC )
dvco.k 
|- ( ph -> K e. V )
dvco.l 
|- ( ph -> L e. V )
dvco.bf 
|- ( ph -> ( G ` C ) ( S _D F ) K )
dvco.bg 
|- ( ph -> C ( T _D G ) L )
dvco.j 
|- J = ( TopOpen ` CCfld )
Assertion dvcobr 
|- ( ph -> C ( T _D ( F o. G ) ) ( K x. L ) )

Proof

Step Hyp Ref Expression
1 dvco.f 
 |-  ( ph -> F : X --> CC )
2 dvco.x 
 |-  ( ph -> X C_ S )
3 dvco.g 
 |-  ( ph -> G : Y --> X )
4 dvco.y 
 |-  ( ph -> Y C_ T )
5 dvcobr.s 
 |-  ( ph -> S C_ CC )
6 dvcobr.t 
 |-  ( ph -> T C_ CC )
7 dvco.k 
 |-  ( ph -> K e. V )
8 dvco.l 
 |-  ( ph -> L e. V )
9 dvco.bf 
 |-  ( ph -> ( G ` C ) ( S _D F ) K )
10 dvco.bg 
 |-  ( ph -> C ( T _D G ) L )
11 dvco.j 
 |-  J = ( TopOpen ` CCfld )
12 eqid 
 |-  ( J |`t T ) = ( J |`t T )
13 eqid 
 |-  ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )
14 2 5 sstrd 
 |-  ( ph -> X C_ CC )
15 3 14 fssd 
 |-  ( ph -> G : Y --> CC )
16 12 11 13 6 15 4 eldv 
 |-  ( ph -> ( C ( T _D G ) L <-> ( C e. ( ( int ` ( J |`t T ) ) ` Y ) /\ L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) ) ) )
17 10 16 mpbid 
 |-  ( ph -> ( C e. ( ( int ` ( J |`t T ) ) ` Y ) /\ L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) ) )
18 17 simpld 
 |-  ( ph -> C e. ( ( int ` ( J |`t T ) ) ` Y ) )
19 5 1 2 dvcl 
 |-  ( ( ph /\ ( G ` C ) ( S _D F ) K ) -> K e. CC )
20 9 19 mpdan 
 |-  ( ph -> K e. CC )
21 20 ad2antrr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> K e. CC )
22 1 adantr 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> F : X --> CC )
23 eldifi 
 |-  ( z e. ( Y \ { C } ) -> z e. Y )
24 ffvelrn 
 |-  ( ( G : Y --> X /\ z e. Y ) -> ( G ` z ) e. X )
25 3 23 24 syl2an 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( G ` z ) e. X )
26 22 25 ffvelrnd 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( F ` ( G ` z ) ) e. CC )
27 26 adantr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( F ` ( G ` z ) ) e. CC )
28 3 adantr 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> G : Y --> X )
29 6 15 4 dvbss 
 |-  ( ph -> dom ( T _D G ) C_ Y )
30 reldv 
 |-  Rel ( T _D G )
31 releldm 
 |-  ( ( Rel ( T _D G ) /\ C ( T _D G ) L ) -> C e. dom ( T _D G ) )
32 30 10 31 sylancr 
 |-  ( ph -> C e. dom ( T _D G ) )
33 29 32 sseldd 
 |-  ( ph -> C e. Y )
34 33 adantr 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> C e. Y )
35 28 34 ffvelrnd 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( G ` C ) e. X )
36 22 35 ffvelrnd 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( F ` ( G ` C ) ) e. CC )
37 36 adantr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( F ` ( G ` C ) ) e. CC )
38 27 37 subcld 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) e. CC )
39 15 ad2antrr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> G : Y --> CC )
40 23 ad2antlr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> z e. Y )
41 39 40 ffvelrnd 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( G ` z ) e. CC )
42 33 ad2antrr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> C e. Y )
43 39 42 ffvelrnd 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( G ` C ) e. CC )
44 41 43 subcld 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( ( G ` z ) - ( G ` C ) ) e. CC )
45 simpr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> -. ( G ` z ) = ( G ` C ) )
46 41 43 subeq0ad 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( ( ( G ` z ) - ( G ` C ) ) = 0 <-> ( G ` z ) = ( G ` C ) ) )
47 46 necon3abid 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( ( ( G ` z ) - ( G ` C ) ) =/= 0 <-> -. ( G ` z ) = ( G ` C ) ) )
48 45 47 mpbird 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( ( G ` z ) - ( G ` C ) ) =/= 0 )
49 38 44 48 divcld 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) e. CC )
50 21 49 ifclda 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) e. CC )
51 4 6 sstrd 
 |-  ( ph -> Y C_ CC )
52 15 51 33 dvlem 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) e. CC )
53 ssidd 
 |-  ( ph -> CC C_ CC )
54 11 cnfldtopon 
 |-  J e. ( TopOn ` CC )
55 txtopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ J e. ( TopOn ` CC ) ) -> ( J tX J ) e. ( TopOn ` ( CC X. CC ) ) )
56 54 54 55 mp2an 
 |-  ( J tX J ) e. ( TopOn ` ( CC X. CC ) )
57 56 toponrestid 
 |-  ( J tX J ) = ( ( J tX J ) |`t ( CC X. CC ) )
58 25 anim1i 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) =/= ( G ` C ) ) -> ( ( G ` z ) e. X /\ ( G ` z ) =/= ( G ` C ) ) )
59 eldifsn 
 |-  ( ( G ` z ) e. ( X \ { ( G ` C ) } ) <-> ( ( G ` z ) e. X /\ ( G ` z ) =/= ( G ` C ) ) )
60 58 59 sylibr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) =/= ( G ` C ) ) -> ( G ` z ) e. ( X \ { ( G ` C ) } ) )
61 60 anasss 
 |-  ( ( ph /\ ( z e. ( Y \ { C } ) /\ ( G ` z ) =/= ( G ` C ) ) ) -> ( G ` z ) e. ( X \ { ( G ` C ) } ) )
62 eldifsni 
 |-  ( y e. ( X \ { ( G ` C ) } ) -> y =/= ( G ` C ) )
63 ifnefalse 
 |-  ( y =/= ( G ` C ) -> if ( y = ( G ` C ) , K , ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) = ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) )
64 62 63 syl 
 |-  ( y e. ( X \ { ( G ` C ) } ) -> if ( y = ( G ` C ) , K , ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) = ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) )
65 64 adantl 
 |-  ( ( ph /\ y e. ( X \ { ( G ` C ) } ) ) -> if ( y = ( G ` C ) , K , ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) = ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) )
66 3 33 ffvelrnd 
 |-  ( ph -> ( G ` C ) e. X )
67 1 14 66 dvlem 
 |-  ( ( ph /\ y e. ( X \ { ( G ` C ) } ) ) -> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) e. CC )
68 65 67 eqeltrd 
 |-  ( ( ph /\ y e. ( X \ { ( G ` C ) } ) ) -> if ( y = ( G ` C ) , K , ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) e. CC )
69 limcresi 
 |-  ( G limCC C ) C_ ( ( G |` ( Y \ { C } ) ) limCC C )
70 3 feqmptd 
 |-  ( ph -> G = ( z e. Y |-> ( G ` z ) ) )
71 70 reseq1d 
 |-  ( ph -> ( G |` ( Y \ { C } ) ) = ( ( z e. Y |-> ( G ` z ) ) |` ( Y \ { C } ) ) )
72 difss 
 |-  ( Y \ { C } ) C_ Y
73 resmpt 
 |-  ( ( Y \ { C } ) C_ Y -> ( ( z e. Y |-> ( G ` z ) ) |` ( Y \ { C } ) ) = ( z e. ( Y \ { C } ) |-> ( G ` z ) ) )
74 72 73 ax-mp 
 |-  ( ( z e. Y |-> ( G ` z ) ) |` ( Y \ { C } ) ) = ( z e. ( Y \ { C } ) |-> ( G ` z ) )
75 71 74 eqtrdi 
 |-  ( ph -> ( G |` ( Y \ { C } ) ) = ( z e. ( Y \ { C } ) |-> ( G ` z ) ) )
76 75 oveq1d 
 |-  ( ph -> ( ( G |` ( Y \ { C } ) ) limCC C ) = ( ( z e. ( Y \ { C } ) |-> ( G ` z ) ) limCC C ) )
77 69 76 sseqtrid 
 |-  ( ph -> ( G limCC C ) C_ ( ( z e. ( Y \ { C } ) |-> ( G ` z ) ) limCC C ) )
78 eqid 
 |-  ( J |`t Y ) = ( J |`t Y )
79 78 11 dvcnp2 
 |-  ( ( ( T C_ CC /\ G : Y --> CC /\ Y C_ T ) /\ C e. dom ( T _D G ) ) -> G e. ( ( ( J |`t Y ) CnP J ) ` C ) )
80 6 15 4 32 79 syl31anc 
 |-  ( ph -> G e. ( ( ( J |`t Y ) CnP J ) ` C ) )
81 11 78 cnplimc 
 |-  ( ( Y C_ CC /\ C e. Y ) -> ( G e. ( ( ( J |`t Y ) CnP J ) ` C ) <-> ( G : Y --> CC /\ ( G ` C ) e. ( G limCC C ) ) ) )
82 51 33 81 syl2anc 
 |-  ( ph -> ( G e. ( ( ( J |`t Y ) CnP J ) ` C ) <-> ( G : Y --> CC /\ ( G ` C ) e. ( G limCC C ) ) ) )
83 80 82 mpbid 
 |-  ( ph -> ( G : Y --> CC /\ ( G ` C ) e. ( G limCC C ) ) )
84 83 simprd 
 |-  ( ph -> ( G ` C ) e. ( G limCC C ) )
85 77 84 sseldd 
 |-  ( ph -> ( G ` C ) e. ( ( z e. ( Y \ { C } ) |-> ( G ` z ) ) limCC C ) )
86 eqid 
 |-  ( J |`t S ) = ( J |`t S )
87 eqid 
 |-  ( y e. ( X \ { ( G ` C ) } ) |-> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) = ( y e. ( X \ { ( G ` C ) } ) |-> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) )
88 86 11 87 5 1 2 eldv 
 |-  ( ph -> ( ( G ` C ) ( S _D F ) K <-> ( ( G ` C ) e. ( ( int ` ( J |`t S ) ) ` X ) /\ K e. ( ( y e. ( X \ { ( G ` C ) } ) |-> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) limCC ( G ` C ) ) ) ) )
89 9 88 mpbid 
 |-  ( ph -> ( ( G ` C ) e. ( ( int ` ( J |`t S ) ) ` X ) /\ K e. ( ( y e. ( X \ { ( G ` C ) } ) |-> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) limCC ( G ` C ) ) ) )
90 89 simprd 
 |-  ( ph -> K e. ( ( y e. ( X \ { ( G ` C ) } ) |-> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) limCC ( G ` C ) ) )
91 64 mpteq2ia 
 |-  ( y e. ( X \ { ( G ` C ) } ) |-> if ( y = ( G ` C ) , K , ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) ) = ( y e. ( X \ { ( G ` C ) } ) |-> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) )
92 91 oveq1i 
 |-  ( ( y e. ( X \ { ( G ` C ) } ) |-> if ( y = ( G ` C ) , K , ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) ) limCC ( G ` C ) ) = ( ( y e. ( X \ { ( G ` C ) } ) |-> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) limCC ( G ` C ) )
93 90 92 eleqtrrdi 
 |-  ( ph -> K e. ( ( y e. ( X \ { ( G ` C ) } ) |-> if ( y = ( G ` C ) , K , ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) ) limCC ( G ` C ) ) )
94 eqeq1 
 |-  ( y = ( G ` z ) -> ( y = ( G ` C ) <-> ( G ` z ) = ( G ` C ) ) )
95 fveq2 
 |-  ( y = ( G ` z ) -> ( F ` y ) = ( F ` ( G ` z ) ) )
96 95 oveq1d 
 |-  ( y = ( G ` z ) -> ( ( F ` y ) - ( F ` ( G ` C ) ) ) = ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) )
97 oveq1 
 |-  ( y = ( G ` z ) -> ( y - ( G ` C ) ) = ( ( G ` z ) - ( G ` C ) ) )
98 96 97 oveq12d 
 |-  ( y = ( G ` z ) -> ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) )
99 94 98 ifbieq2d 
 |-  ( y = ( G ` z ) -> if ( y = ( G ` C ) , K , ( ( ( F ` y ) - ( F ` ( G ` C ) ) ) / ( y - ( G ` C ) ) ) ) = if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) )
100 iftrue 
 |-  ( ( G ` z ) = ( G ` C ) -> if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) = K )
101 100 ad2antll 
 |-  ( ( ph /\ ( z e. ( Y \ { C } ) /\ ( G ` z ) = ( G ` C ) ) ) -> if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) = K )
102 61 68 85 93 99 101 limcco 
 |-  ( ph -> K e. ( ( z e. ( Y \ { C } ) |-> if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) ) limCC C ) )
103 17 simprd 
 |-  ( ph -> L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) )
104 11 mulcn 
 |-  x. e. ( ( J tX J ) Cn J )
105 6 15 4 dvcl 
 |-  ( ( ph /\ C ( T _D G ) L ) -> L e. CC )
106 10 105 mpdan 
 |-  ( ph -> L e. CC )
107 20 106 opelxpd 
 |-  ( ph -> <. K , L >. e. ( CC X. CC ) )
108 56 toponunii 
 |-  ( CC X. CC ) = U. ( J tX J )
109 108 cncnpi 
 |-  ( ( x. e. ( ( J tX J ) Cn J ) /\ <. K , L >. e. ( CC X. CC ) ) -> x. e. ( ( ( J tX J ) CnP J ) ` <. K , L >. ) )
110 104 107 109 sylancr 
 |-  ( ph -> x. e. ( ( ( J tX J ) CnP J ) ` <. K , L >. ) )
111 50 52 53 53 11 57 102 103 110 limccnp2 
 |-  ( ph -> ( K x. L ) e. ( ( z e. ( Y \ { C } ) |-> ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) ) limCC C ) )
112 oveq1 
 |-  ( K = if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) -> ( K x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) )
113 112 eqeq1d 
 |-  ( K = if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) -> ( ( K x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) <-> ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) ) )
114 oveq1 
 |-  ( ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) = if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) -> ( ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) )
115 114 eqeq1d 
 |-  ( ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) = if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) -> ( ( ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) <-> ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) ) )
116 21 mul01d 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( K x. 0 ) = 0 )
117 14 adantr 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> X C_ CC )
118 117 25 sseldd 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( G ` z ) e. CC )
119 117 35 sseldd 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( G ` C ) e. CC )
120 118 119 subeq0ad 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) = 0 <-> ( G ` z ) = ( G ` C ) ) )
121 120 biimpar 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( G ` z ) - ( G ` C ) ) = 0 )
122 121 oveq1d 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) = ( 0 / ( z - C ) ) )
123 51 adantr 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> Y C_ CC )
124 23 adantl 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> z e. Y )
125 123 124 sseldd 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> z e. CC )
126 123 34 sseldd 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> C e. CC )
127 125 126 subcld 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( z - C ) e. CC )
128 eldifsni 
 |-  ( z e. ( Y \ { C } ) -> z =/= C )
129 128 adantl 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> z =/= C )
130 125 126 129 subne0d 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( z - C ) =/= 0 )
131 127 130 div0d 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( 0 / ( z - C ) ) = 0 )
132 131 adantr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( 0 / ( z - C ) ) = 0 )
133 122 132 eqtrd 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) = 0 )
134 133 oveq2d 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( K x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( K x. 0 ) )
135 fveq2 
 |-  ( ( G ` z ) = ( G ` C ) -> ( F ` ( G ` z ) ) = ( F ` ( G ` C ) ) )
136 26 36 subeq0ad 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) = 0 <-> ( F ` ( G ` z ) ) = ( F ` ( G ` C ) ) ) )
137 135 136 syl5ibr 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( G ` z ) = ( G ` C ) -> ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) = 0 ) )
138 137 imp 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) = 0 )
139 138 oveq1d 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) = ( 0 / ( z - C ) ) )
140 139 132 eqtrd 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) = 0 )
141 116 134 140 3eqtr4d 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( K x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) )
142 127 adantr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( z - C ) e. CC )
143 130 adantr 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( z - C ) =/= 0 )
144 38 44 142 48 143 dmdcan2d 
 |-  ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) )
145 113 115 141 144 ifbothda 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) )
146 fvco3 
 |-  ( ( G : Y --> X /\ z e. Y ) -> ( ( F o. G ) ` z ) = ( F ` ( G ` z ) ) )
147 3 23 146 syl2an 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( F o. G ) ` z ) = ( F ` ( G ` z ) ) )
148 fvco3 
 |-  ( ( G : Y --> X /\ C e. Y ) -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
149 3 33 148 syl2anc 
 |-  ( ph -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
150 149 adantr 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
151 147 150 oveq12d 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) = ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) )
152 151 oveq1d 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) )
153 145 152 eqtr4d 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) )
154 153 mpteq2dva 
 |-  ( ph -> ( z e. ( Y \ { C } ) |-> ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) ) = ( z e. ( Y \ { C } ) |-> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) ) )
155 154 oveq1d 
 |-  ( ph -> ( ( z e. ( Y \ { C } ) |-> ( if ( ( G ` z ) = ( G ` C ) , K , ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( ( G ` z ) - ( G ` C ) ) ) ) x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) ) limCC C ) = ( ( z e. ( Y \ { C } ) |-> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) ) limCC C ) )
156 111 155 eleqtrd 
 |-  ( ph -> ( K x. L ) e. ( ( z e. ( Y \ { C } ) |-> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) ) limCC C ) )
157 eqid 
 |-  ( z e. ( Y \ { C } ) |-> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) ) = ( z e. ( Y \ { C } ) |-> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) )
158 fco 
 |-  ( ( F : X --> CC /\ G : Y --> X ) -> ( F o. G ) : Y --> CC )
159 1 3 158 syl2anc 
 |-  ( ph -> ( F o. G ) : Y --> CC )
160 12 11 157 6 159 4 eldv 
 |-  ( ph -> ( C ( T _D ( F o. G ) ) ( K x. L ) <-> ( C e. ( ( int ` ( J |`t T ) ) ` Y ) /\ ( K x. L ) e. ( ( z e. ( Y \ { C } ) |-> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) ) limCC C ) ) ) )
161 18 156 160 mpbir2and 
 |-  ( ph -> C ( T _D ( F o. G ) ) ( K x. L ) )