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) Avoid ax-mulf and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025)

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