Theorem gg-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 . (Revised by GG, 16-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		gg-dvco.f	|- ( ph -> F : X --> CC )
2		gg-dvco.x	|- ( ph -> X C_ S )
3		gg-dvco.g	|- ( ph -> G : Y --> X )
4		gg-dvco.y	|- ( ph -> Y C_ T )
5		gg-dvcobr.s	|- ( ph -> S C_ CC )
6		gg-dvcobr.t	|- ( ph -> T C_ CC )
7		gg-dvco.k	|- ( ph -> K e. V )
8		gg-dvco.l	|- ( ph -> L e. V )
9		gg-dvco.bf	|- ( ph -> ( G ` C ) ( S _D F ) K )
10		gg-dvco.bg	|- ( ph -> C ( T _D G ) L )
11		gg-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		ffvelcdm	|- ( ( 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	ffvelcdmd	|- ( ( 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	ffvelcdmd	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( G ` C ) e. X )
36	22 35	ffvelcdmd	|- ( ( 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	ffvelcdmd	|- ( ( ( 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	ffvelcdmd	|- ( ( ( 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	ffvelcdmd	|- ( 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	gg-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	mpomulcn	|- ( u e. CC , v e. CC |-> ( u x. v ) ) 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	|- ( ( ( 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 >. ) )
110	104 107 109	sylancr	|- ( ph -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( J tX J ) CnP J ) ` <. K , L >. ) )
111	50 52 53 53 11 57 102 103 110	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 ) )
112		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 ) ) ) ) }
113	112	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 )
114	111 113	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 ) )
115		ovmul	|- ( ( K e. CC /\ L e. CC ) -> ( K ( u e. CC , v e. CC |-> ( u x. v ) ) L ) = ( K x. L ) )
116	20 106 115	syl2anc	|- ( ph -> ( K ( u e. CC , v e. CC |-> ( u x. v ) ) L ) = ( K x. L ) )
117		ovmul	|- ( ( 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 ) ) ) )
118	50 52 117	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 ) ) ) )
119	118	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 ) ) ) ) )
120	119	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 ) ) ) ) ) )
121	120	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 ) ) ) ) } )
122		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 ) ) ) ) }
123	122	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 ) ) ) )
124	123	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 ) ) ) ) )
125	124	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 ) ) ) ) )
126	125	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 ) )
127	121 126	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 ) )
128	114 116 127	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 ) )
129		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 ) ) ) )
130	129	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 ) ) ) )
131		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 ) ) ) )
132	131	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 ) ) ) )
133	21	mul01d	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( K x. 0 ) = 0 )
134	14	adantr	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> X C_ CC )
135	134 25	sseldd	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( G ` z ) e. CC )
136	134 35	sseldd	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( G ` C ) e. CC )
137	135 136	subeq0ad	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) = 0 <-> ( G ` z ) = ( G ` C ) ) )
138	137	biimpar	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( G ` z ) - ( G ` C ) ) = 0 )
139	138	oveq1d	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) = ( 0 / ( z - C ) ) )
140	51	adantr	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> Y C_ CC )
141	23	adantl	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> z e. Y )
142	140 141	sseldd	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> z e. CC )
143	140 34	sseldd	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> C e. CC )
144	142 143	subcld	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( z - C ) e. CC )
145		eldifsni	|- ( z e. ( Y \ { C } ) -> z =/= C )
146	145	adantl	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> z =/= C )
147	142 143 146	subne0d	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( z - C ) =/= 0 )
148	144 147	div0d	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( 0 / ( z - C ) ) = 0 )
149	148	adantr	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( 0 / ( z - C ) ) = 0 )
150	139 149	eqtrd	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) = 0 )
151	150	oveq2d	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( K x. ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( K x. 0 ) )
152		fveq2	|- ( ( G ` z ) = ( G ` C ) -> ( F ` ( G ` z ) ) = ( F ` ( G ` C ) ) )
153	26 36	subeq0ad	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) = 0 <-> ( F ` ( G ` z ) ) = ( F ` ( G ` C ) ) ) )
154	152 153	imbitrrid	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( G ` z ) = ( G ` C ) -> ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) = 0 ) )
155	154	imp	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) = 0 )
156	155	oveq1d	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) = ( 0 / ( z - C ) ) )
157	156 149	eqtrd	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ ( G ` z ) = ( G ` C ) ) -> ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) = 0 )
158	133 151 157	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 ) ) )
159	144	adantr	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( z - C ) e. CC )
160	147	adantr	|- ( ( ( ph /\ z e. ( Y \ { C } ) ) /\ -. ( G ` z ) = ( G ` C ) ) -> ( z - C ) =/= 0 )
161	38 44 159 48 160	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 ) ) )
162	130 132 158 161	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 ) ) )
163		fvco3	|- ( ( G : Y --> X /\ z e. Y ) -> ( ( F o. G ) ` z ) = ( F ` ( G ` z ) ) )
164	3 23 163	syl2an	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( F o. G ) ` z ) = ( F ` ( G ` z ) ) )
165	3 33	fvco3d	|- ( ph -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
166	165	adantr	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
167	164 166	oveq12d	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) = ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) )
168	167	oveq1d	|- ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) = ( ( ( F ` ( G ` z ) ) - ( F ` ( G ` C ) ) ) / ( z - C ) ) )
169	162 168	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 ) ) )
170	169	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 ) ) ) )
171	170	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 ) )
172	128 171	eleqtrd	|- ( ph -> ( K x. L ) e. ( ( z e. ( Y \ { C } ) |-> ( ( ( ( F o. G ) ` z ) - ( ( F o. G ) ` C ) ) / ( z - C ) ) ) limCC C ) )
173		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 ) ) )
174	1 3	fcod	|- ( ph -> ( F o. G ) : Y --> CC )
175	12 11 173 6 174 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 ) ) ) )
176	18 172 175	mpbir2and	|- ( ph -> C ( T _D ( F o. G ) ) ( K x. L ) )