Metamath Proof Explorer

Theorem dvmulbr

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

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

Proof

Step Hyp Ref Expression
1 dvadd.f 
 |-  ( ph -> F : X --> CC )
2 dvadd.x 
 |-  ( ph -> X C_ S )
3 dvadd.g 
 |-  ( ph -> G : Y --> CC )
4 dvadd.y 
 |-  ( ph -> Y C_ S )
5 dvaddbr.s 
 |-  ( ph -> S C_ CC )
6 dvadd.k 
 |-  ( ph -> K e. V )
7 dvadd.l 
 |-  ( ph -> L e. V )
8 dvadd.bf 
 |-  ( ph -> C ( S _D F ) K )
9 dvadd.bg 
 |-  ( ph -> C ( S _D G ) L )
10 dvadd.j 
 |-  J = ( TopOpen ` CCfld )
11 eqid 
 |-  ( J |`t S ) = ( J |`t S )
12 eqid 
 |-  ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) = ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) )
13 11 10 12 5 1 2 eldv 
 |-  ( ph -> ( C ( S _D F ) K <-> ( C e. ( ( int ` ( J |`t S ) ) ` X ) /\ K e. ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) limCC C ) ) ) )
14 8 13 mpbid 
 |-  ( ph -> ( C e. ( ( int ` ( J |`t S ) ) ` X ) /\ K e. ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) limCC C ) ) )
15 14 simpld 
 |-  ( ph -> C e. ( ( int ` ( J |`t S ) ) ` X ) )
16 eqid 
 |-  ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )
17 11 10 16 5 3 4 eldv 
 |-  ( ph -> ( C ( S _D G ) L <-> ( C e. ( ( int ` ( J |`t S ) ) ` Y ) /\ L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) ) ) )
18 9 17 mpbid 
 |-  ( ph -> ( C e. ( ( int ` ( J |`t S ) ) ` Y ) /\ L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) ) )
19 18 simpld 
 |-  ( ph -> C e. ( ( int ` ( J |`t S ) ) ` Y ) )
20 15 19 elind 
 |-  ( ph -> C e. ( ( ( int ` ( J |`t S ) ) ` X ) i^i ( ( int ` ( J |`t S ) ) ` Y ) ) )
21 10 cnfldtopon 
 |-  J e. ( TopOn ` CC )
22 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ S C_ CC ) -> ( J |`t S ) e. ( TopOn ` S ) )
23 21 5 22 sylancr 
 |-  ( ph -> ( J |`t S ) e. ( TopOn ` S ) )
24 topontop 
 |-  ( ( J |`t S ) e. ( TopOn ` S ) -> ( J |`t S ) e. Top )
25 23 24 syl 
 |-  ( ph -> ( J |`t S ) e. Top )
26 toponuni 
 |-  ( ( J |`t S ) e. ( TopOn ` S ) -> S = U. ( J |`t S ) )
27 23 26 syl 
 |-  ( ph -> S = U. ( J |`t S ) )
28 2 27 sseqtrd 
 |-  ( ph -> X C_ U. ( J |`t S ) )
29 4 27 sseqtrd 
 |-  ( ph -> Y C_ U. ( J |`t S ) )
30 eqid 
 |-  U. ( J |`t S ) = U. ( J |`t S )
31 30 ntrin 
 |-  ( ( ( J |`t S ) e. Top /\ X C_ U. ( J |`t S ) /\ Y C_ U. ( J |`t S ) ) -> ( ( int ` ( J |`t S ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J |`t S ) ) ` X ) i^i ( ( int ` ( J |`t S ) ) ` Y ) ) )
32 25 28 29 31 syl3anc 
 |-  ( ph -> ( ( int ` ( J |`t S ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J |`t S ) ) ` X ) i^i ( ( int ` ( J |`t S ) ) ` Y ) ) )
33 20 32 eleqtrrd 
 |-  ( ph -> C e. ( ( int ` ( J |`t S ) ) ` ( X i^i Y ) ) )
34 1 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> F : X --> CC )
35 inss1 
 |-  ( X i^i Y ) C_ X
36 eldifi 
 |-  ( z e. ( ( X i^i Y ) \ { C } ) -> z e. ( X i^i Y ) )
37 36 adantl 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. ( X i^i Y ) )
38 35 37 sselid 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. X )
39 34 38 ffvelrnd 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( F ` z ) e. CC )
40 5 1 2 dvbss 
 |-  ( ph -> dom ( S _D F ) C_ X )
41 reldv 
 |-  Rel ( S _D F )
42 releldm 
 |-  ( ( Rel ( S _D F ) /\ C ( S _D F ) K ) -> C e. dom ( S _D F ) )
43 41 8 42 sylancr 
 |-  ( ph -> C e. dom ( S _D F ) )
44 40 43 sseldd 
 |-  ( ph -> C e. X )
45 1 44 ffvelrnd 
 |-  ( ph -> ( F ` C ) e. CC )
46 45 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( F ` C ) e. CC )
47 39 46 subcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F ` z ) - ( F ` C ) ) e. CC )
48 2 5 sstrd 
 |-  ( ph -> X C_ CC )
49 48 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> X C_ CC )
50 49 38 sseldd 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. CC )
51 48 44 sseldd 
 |-  ( ph -> C e. CC )
52 51 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> C e. CC )
53 50 52 subcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( z - C ) e. CC )
54 eldifsni 
 |-  ( z e. ( ( X i^i Y ) \ { C } ) -> z =/= C )
55 54 adantl 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z =/= C )
56 50 52 55 subne0d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( z - C ) =/= 0 )
57 47 53 56 divcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) e. CC )
58 3 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> G : Y --> CC )
59 inss2 
 |-  ( X i^i Y ) C_ Y
60 59 37 sselid 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. Y )
61 58 60 ffvelrnd 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( G ` z ) e. CC )
62 57 61 mulcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) x. ( G ` z ) ) e. CC )
63 ssdif 
 |-  ( ( X i^i Y ) C_ Y -> ( ( X i^i Y ) \ { C } ) C_ ( Y \ { C } ) )
64 59 63 mp1i 
 |-  ( ph -> ( ( X i^i Y ) \ { C } ) C_ ( Y \ { C } ) )
65 64 sselda 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> z e. ( Y \ { C } ) )
66 4 5 sstrd 
 |-  ( ph -> Y C_ CC )
67 5 3 4 dvbss 
 |-  ( ph -> dom ( S _D G ) C_ Y )
68 reldv 
 |-  Rel ( S _D G )
69 releldm 
 |-  ( ( Rel ( S _D G ) /\ C ( S _D G ) L ) -> C e. dom ( S _D G ) )
70 68 9 69 sylancr 
 |-  ( ph -> C e. dom ( S _D G ) )
71 67 70 sseldd 
 |-  ( ph -> C e. Y )
72 3 66 71 dvlem 
 |-  ( ( ph /\ z e. ( Y \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) e. CC )
73 65 72 syldan 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) e. CC )
74 73 46 mulcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) x. ( F ` C ) ) e. CC )
75 ssidd 
 |-  ( ph -> CC C_ CC )
76 txtopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ J e. ( TopOn ` CC ) ) -> ( J tX J ) e. ( TopOn ` ( CC X. CC ) ) )
77 21 21 76 mp2an 
 |-  ( J tX J ) e. ( TopOn ` ( CC X. CC ) )
78 77 toponrestid 
 |-  ( J tX J ) = ( ( J tX J ) |`t ( CC X. CC ) )
79 14 simprd 
 |-  ( ph -> K e. ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) limCC C ) )
80 1 48 44 dvlem 
 |-  ( ( ph /\ z e. ( X \ { C } ) ) -> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) e. CC )
81 80 fmpttd 
 |-  ( ph -> ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) : ( X \ { C } ) --> CC )
82 ssdif 
 |-  ( ( X i^i Y ) C_ X -> ( ( X i^i Y ) \ { C } ) C_ ( X \ { C } ) )
83 35 82 mp1i 
 |-  ( ph -> ( ( X i^i Y ) \ { C } ) C_ ( X \ { C } ) )
84 48 ssdifssd 
 |-  ( ph -> ( X \ { C } ) C_ CC )
85 eqid 
 |-  ( J |`t ( ( X \ { C } ) u. { C } ) ) = ( J |`t ( ( X \ { C } ) u. { C } ) )
86 35 2 sstrid 
 |-  ( ph -> ( X i^i Y ) C_ S )
87 86 27 sseqtrd 
 |-  ( ph -> ( X i^i Y ) C_ U. ( J |`t S ) )
88 difssd 
 |-  ( ph -> ( U. ( J |`t S ) \ X ) C_ U. ( J |`t S ) )
89 87 88 unssd 
 |-  ( ph -> ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) C_ U. ( J |`t S ) )
90 ssun1 
 |-  ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) )
91 90 a1i 
 |-  ( ph -> ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) )
92 30 ntrss 
 |-  ( ( ( J |`t S ) e. Top /\ ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) C_ U. ( J |`t S ) /\ ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) ) -> ( ( int ` ( J |`t S ) ) ` ( X i^i Y ) ) C_ ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) ) )
93 25 89 91 92 syl3anc 
 |-  ( ph -> ( ( int ` ( J |`t S ) ) ` ( X i^i Y ) ) C_ ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) ) )
94 93 33 sseldd 
 |-  ( ph -> C e. ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) ) )
95 94 44 elind 
 |-  ( ph -> C e. ( ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) ) i^i X ) )
96 35 a1i 
 |-  ( ph -> ( X i^i Y ) C_ X )
97 eqid 
 |-  ( ( J |`t S ) |`t X ) = ( ( J |`t S ) |`t X )
98 30 97 restntr 
 |-  ( ( ( J |`t S ) e. Top /\ X C_ U. ( J |`t S ) /\ ( X i^i Y ) C_ X ) -> ( ( int ` ( ( J |`t S ) |`t X ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) ) i^i X ) )
99 25 28 96 98 syl3anc 
 |-  ( ph -> ( ( int ` ( ( J |`t S ) |`t X ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) ) i^i X ) )
100 10 cnfldtop 
 |-  J e. Top
101 100 a1i 
 |-  ( ph -> J e. Top )
102 cnex 
 |-  CC e. _V
103 ssexg 
 |-  ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
104 5 102 103 sylancl 
 |-  ( ph -> S e. _V )
105 restabs 
 |-  ( ( J e. Top /\ X C_ S /\ S e. _V ) -> ( ( J |`t S ) |`t X ) = ( J |`t X ) )
106 101 2 104 105 syl3anc 
 |-  ( ph -> ( ( J |`t S ) |`t X ) = ( J |`t X ) )
107 106 fveq2d 
 |-  ( ph -> ( int ` ( ( J |`t S ) |`t X ) ) = ( int ` ( J |`t X ) ) )
108 107 fveq1d 
 |-  ( ph -> ( ( int ` ( ( J |`t S ) |`t X ) ) ` ( X i^i Y ) ) = ( ( int ` ( J |`t X ) ) ` ( X i^i Y ) ) )
109 99 108 eqtr3d 
 |-  ( ph -> ( ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ X ) ) ) i^i X ) = ( ( int ` ( J |`t X ) ) ` ( X i^i Y ) ) )
110 95 109 eleqtrd 
 |-  ( ph -> C e. ( ( int ` ( J |`t X ) ) ` ( X i^i Y ) ) )
111 undif1 
 |-  ( ( X \ { C } ) u. { C } ) = ( X u. { C } )
112 44 snssd 
 |-  ( ph -> { C } C_ X )
113 ssequn2 
 |-  ( { C } C_ X <-> ( X u. { C } ) = X )
114 112 113 sylib 
 |-  ( ph -> ( X u. { C } ) = X )
115 111 114 syl5eq 
 |-  ( ph -> ( ( X \ { C } ) u. { C } ) = X )
116 115 oveq2d 
 |-  ( ph -> ( J |`t ( ( X \ { C } ) u. { C } ) ) = ( J |`t X ) )
117 116 fveq2d 
 |-  ( ph -> ( int ` ( J |`t ( ( X \ { C } ) u. { C } ) ) ) = ( int ` ( J |`t X ) ) )
118 undif1 
 |-  ( ( ( X i^i Y ) \ { C } ) u. { C } ) = ( ( X i^i Y ) u. { C } )
119 44 71 elind 
 |-  ( ph -> C e. ( X i^i Y ) )
120 119 snssd 
 |-  ( ph -> { C } C_ ( X i^i Y ) )
121 ssequn2 
 |-  ( { C } C_ ( X i^i Y ) <-> ( ( X i^i Y ) u. { C } ) = ( X i^i Y ) )
122 120 121 sylib 
 |-  ( ph -> ( ( X i^i Y ) u. { C } ) = ( X i^i Y ) )
123 118 122 syl5eq 
 |-  ( ph -> ( ( ( X i^i Y ) \ { C } ) u. { C } ) = ( X i^i Y ) )
124 117 123 fveq12d 
 |-  ( ph -> ( ( int ` ( J |`t ( ( X \ { C } ) u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) = ( ( int ` ( J |`t X ) ) ` ( X i^i Y ) ) )
125 110 124 eleqtrrd 
 |-  ( ph -> C e. ( ( int ` ( J |`t ( ( X \ { C } ) u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) )
126 81 83 84 10 85 125 limcres 
 |-  ( ph -> ( ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) limCC C ) = ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) limCC C ) )
127 83 resmptd 
 |-  ( ph -> ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) )
128 127 oveq1d 
 |-  ( ph -> ( ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) limCC C ) )
129 126 128 eqtr3d 
 |-  ( ph -> ( ( z e. ( X \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) limCC C ) )
130 79 129 eleqtrd 
 |-  ( ph -> K e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) ) limCC C ) )
131 eqid 
 |-  ( J |`t Y ) = ( J |`t Y )
132 131 10 dvcnp2 
 |-  ( ( ( S C_ CC /\ G : Y --> CC /\ Y C_ S ) /\ C e. dom ( S _D G ) ) -> G e. ( ( ( J |`t Y ) CnP J ) ` C ) )
133 5 3 4 70 132 syl31anc 
 |-  ( ph -> G e. ( ( ( J |`t Y ) CnP J ) ` C ) )
134 10 131 cnplimc 
 |-  ( ( Y C_ CC /\ C e. Y ) -> ( G e. ( ( ( J |`t Y ) CnP J ) ` C ) <-> ( G : Y --> CC /\ ( G ` C ) e. ( G limCC C ) ) ) )
135 66 71 134 syl2anc 
 |-  ( ph -> ( G e. ( ( ( J |`t Y ) CnP J ) ` C ) <-> ( G : Y --> CC /\ ( G ` C ) e. ( G limCC C ) ) ) )
136 133 135 mpbid 
 |-  ( ph -> ( G : Y --> CC /\ ( G ` C ) e. ( G limCC C ) ) )
137 136 simprd 
 |-  ( ph -> ( G ` C ) e. ( G limCC C ) )
138 difss 
 |-  ( ( X i^i Y ) \ { C } ) C_ ( X i^i Y )
139 138 59 sstri 
 |-  ( ( X i^i Y ) \ { C } ) C_ Y
140 139 a1i 
 |-  ( ph -> ( ( X i^i Y ) \ { C } ) C_ Y )
141 eqid 
 |-  ( J |`t ( Y u. { C } ) ) = ( J |`t ( Y u. { C } ) )
142 difssd 
 |-  ( ph -> ( U. ( J |`t S ) \ Y ) C_ U. ( J |`t S ) )
143 87 142 unssd 
 |-  ( ph -> ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) C_ U. ( J |`t S ) )
144 ssun1 
 |-  ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) )
145 144 a1i 
 |-  ( ph -> ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) )
146 30 ntrss 
 |-  ( ( ( J |`t S ) e. Top /\ ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) C_ U. ( J |`t S ) /\ ( X i^i Y ) C_ ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) ) -> ( ( int ` ( J |`t S ) ) ` ( X i^i Y ) ) C_ ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) ) )
147 25 143 145 146 syl3anc 
 |-  ( ph -> ( ( int ` ( J |`t S ) ) ` ( X i^i Y ) ) C_ ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) ) )
148 147 33 sseldd 
 |-  ( ph -> C e. ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) ) )
149 148 71 elind 
 |-  ( ph -> C e. ( ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) ) i^i Y ) )
150 59 a1i 
 |-  ( ph -> ( X i^i Y ) C_ Y )
151 eqid 
 |-  ( ( J |`t S ) |`t Y ) = ( ( J |`t S ) |`t Y )
152 30 151 restntr 
 |-  ( ( ( J |`t S ) e. Top /\ Y C_ U. ( J |`t S ) /\ ( X i^i Y ) C_ Y ) -> ( ( int ` ( ( J |`t S ) |`t Y ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) ) i^i Y ) )
153 25 29 150 152 syl3anc 
 |-  ( ph -> ( ( int ` ( ( J |`t S ) |`t Y ) ) ` ( X i^i Y ) ) = ( ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) ) i^i Y ) )
154 restabs 
 |-  ( ( J e. Top /\ Y C_ S /\ S e. _V ) -> ( ( J |`t S ) |`t Y ) = ( J |`t Y ) )
155 101 4 104 154 syl3anc 
 |-  ( ph -> ( ( J |`t S ) |`t Y ) = ( J |`t Y ) )
156 155 fveq2d 
 |-  ( ph -> ( int ` ( ( J |`t S ) |`t Y ) ) = ( int ` ( J |`t Y ) ) )
157 156 fveq1d 
 |-  ( ph -> ( ( int ` ( ( J |`t S ) |`t Y ) ) ` ( X i^i Y ) ) = ( ( int ` ( J |`t Y ) ) ` ( X i^i Y ) ) )
158 153 157 eqtr3d 
 |-  ( ph -> ( ( ( int ` ( J |`t S ) ) ` ( ( X i^i Y ) u. ( U. ( J |`t S ) \ Y ) ) ) i^i Y ) = ( ( int ` ( J |`t Y ) ) ` ( X i^i Y ) ) )
159 149 158 eleqtrd 
 |-  ( ph -> C e. ( ( int ` ( J |`t Y ) ) ` ( X i^i Y ) ) )
160 71 snssd 
 |-  ( ph -> { C } C_ Y )
161 ssequn2 
 |-  ( { C } C_ Y <-> ( Y u. { C } ) = Y )
162 160 161 sylib 
 |-  ( ph -> ( Y u. { C } ) = Y )
163 162 oveq2d 
 |-  ( ph -> ( J |`t ( Y u. { C } ) ) = ( J |`t Y ) )
164 163 fveq2d 
 |-  ( ph -> ( int ` ( J |`t ( Y u. { C } ) ) ) = ( int ` ( J |`t Y ) ) )
165 164 123 fveq12d 
 |-  ( ph -> ( ( int ` ( J |`t ( Y u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) = ( ( int ` ( J |`t Y ) ) ` ( X i^i Y ) ) )
166 159 165 eleqtrrd 
 |-  ( ph -> C e. ( ( int ` ( J |`t ( Y u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) )
167 3 140 66 10 141 166 limcres 
 |-  ( ph -> ( ( G |` ( ( X i^i Y ) \ { C } ) ) limCC C ) = ( G limCC C ) )
168 3 140 feqresmpt 
 |-  ( ph -> ( G |` ( ( X i^i Y ) \ { C } ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( G ` z ) ) )
169 168 oveq1d 
 |-  ( ph -> ( ( G |` ( ( X i^i Y ) \ { C } ) ) limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( G ` z ) ) limCC C ) )
170 167 169 eqtr3d 
 |-  ( ph -> ( G limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( G ` z ) ) limCC C ) )
171 137 170 eleqtrd 
 |-  ( ph -> ( G ` C ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( G ` z ) ) limCC C ) )
172 10 mulcn 
 |-  x. e. ( ( J tX J ) Cn J )
173 5 1 2 dvcl 
 |-  ( ( ph /\ C ( S _D F ) K ) -> K e. CC )
174 8 173 mpdan 
 |-  ( ph -> K e. CC )
175 3 71 ffvelrnd 
 |-  ( ph -> ( G ` C ) e. CC )
176 174 175 opelxpd 
 |-  ( ph -> <. K , ( G ` C ) >. e. ( CC X. CC ) )
177 77 toponunii 
 |-  ( CC X. CC ) = U. ( J tX J )
178 177 cncnpi 
 |-  ( ( x. e. ( ( J tX J ) Cn J ) /\ <. K , ( G ` C ) >. e. ( CC X. CC ) ) -> x. e. ( ( ( J tX J ) CnP J ) ` <. K , ( G ` C ) >. ) )
179 172 176 178 sylancr 
 |-  ( ph -> x. e. ( ( ( J tX J ) CnP J ) ` <. K , ( G ` C ) >. ) )
180 57 61 75 75 10 78 130 171 179 limccnp2 
 |-  ( ph -> ( K x. ( G ` C ) ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) x. ( G ` z ) ) ) limCC C ) )
181 18 simprd 
 |-  ( ph -> L e. ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) )
182 72 fmpttd 
 |-  ( ph -> ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) : ( Y \ { C } ) --> CC )
183 66 ssdifssd 
 |-  ( ph -> ( Y \ { C } ) C_ CC )
184 eqid 
 |-  ( J |`t ( ( Y \ { C } ) u. { C } ) ) = ( J |`t ( ( Y \ { C } ) u. { C } ) )
185 undif1 
 |-  ( ( Y \ { C } ) u. { C } ) = ( Y u. { C } )
186 185 162 syl5eq 
 |-  ( ph -> ( ( Y \ { C } ) u. { C } ) = Y )
187 186 oveq2d 
 |-  ( ph -> ( J |`t ( ( Y \ { C } ) u. { C } ) ) = ( J |`t Y ) )
188 187 fveq2d 
 |-  ( ph -> ( int ` ( J |`t ( ( Y \ { C } ) u. { C } ) ) ) = ( int ` ( J |`t Y ) ) )
189 188 123 fveq12d 
 |-  ( ph -> ( ( int ` ( J |`t ( ( Y \ { C } ) u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) = ( ( int ` ( J |`t Y ) ) ` ( X i^i Y ) ) )
190 159 189 eleqtrrd 
 |-  ( ph -> C e. ( ( int ` ( J |`t ( ( Y \ { C } ) u. { C } ) ) ) ` ( ( ( X i^i Y ) \ { C } ) u. { C } ) ) )
191 182 64 183 10 184 190 limcres 
 |-  ( ph -> ( ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) limCC C ) = ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) )
192 64 resmptd 
 |-  ( ph -> ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) )
193 192 oveq1d 
 |-  ( ph -> ( ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) |` ( ( X i^i Y ) \ { C } ) ) limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) )
194 191 193 eqtr3d 
 |-  ( ph -> ( ( z e. ( Y \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) )
195 181 194 eleqtrd 
 |-  ( ph -> L e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) )
196 86 5 sstrd 
 |-  ( ph -> ( X i^i Y ) C_ CC )
197 cncfmptc 
 |-  ( ( ( F ` C ) e. CC /\ ( X i^i Y ) C_ CC /\ CC C_ CC ) -> ( z e. ( X i^i Y ) |-> ( F ` C ) ) e. ( ( X i^i Y ) -cn-> CC ) )
198 45 196 75 197 syl3anc 
 |-  ( ph -> ( z e. ( X i^i Y ) |-> ( F ` C ) ) e. ( ( X i^i Y ) -cn-> CC ) )
199 eqidd 
 |-  ( z = C -> ( F ` C ) = ( F ` C ) )
200 198 119 199 cnmptlimc 
 |-  ( ph -> ( F ` C ) e. ( ( z e. ( X i^i Y ) |-> ( F ` C ) ) limCC C ) )
201 45 adantr 
 |-  ( ( ph /\ z e. ( X i^i Y ) ) -> ( F ` C ) e. CC )
202 201 fmpttd 
 |-  ( ph -> ( z e. ( X i^i Y ) |-> ( F ` C ) ) : ( X i^i Y ) --> CC )
203 202 limcdif 
 |-  ( ph -> ( ( z e. ( X i^i Y ) |-> ( F ` C ) ) limCC C ) = ( ( ( z e. ( X i^i Y ) |-> ( F ` C ) ) |` ( ( X i^i Y ) \ { C } ) ) limCC C ) )
204 resmpt 
 |-  ( ( ( X i^i Y ) \ { C } ) C_ ( X i^i Y ) -> ( ( z e. ( X i^i Y ) |-> ( F ` C ) ) |` ( ( X i^i Y ) \ { C } ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( F ` C ) ) )
205 138 204 mp1i 
 |-  ( ph -> ( ( z e. ( X i^i Y ) |-> ( F ` C ) ) |` ( ( X i^i Y ) \ { C } ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( F ` C ) ) )
206 205 oveq1d 
 |-  ( ph -> ( ( ( z e. ( X i^i Y ) |-> ( F ` C ) ) |` ( ( X i^i Y ) \ { C } ) ) limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( F ` C ) ) limCC C ) )
207 203 206 eqtrd 
 |-  ( ph -> ( ( z e. ( X i^i Y ) |-> ( F ` C ) ) limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( F ` C ) ) limCC C ) )
208 200 207 eleqtrd 
 |-  ( ph -> ( F ` C ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( F ` C ) ) limCC C ) )
209 5 3 4 dvcl 
 |-  ( ( ph /\ C ( S _D G ) L ) -> L e. CC )
210 9 209 mpdan 
 |-  ( ph -> L e. CC )
211 210 45 opelxpd 
 |-  ( ph -> <. L , ( F ` C ) >. e. ( CC X. CC ) )
212 177 cncnpi 
 |-  ( ( x. e. ( ( J tX J ) Cn J ) /\ <. L , ( F ` C ) >. e. ( CC X. CC ) ) -> x. e. ( ( ( J tX J ) CnP J ) ` <. L , ( F ` C ) >. ) )
213 172 211 212 sylancr 
 |-  ( ph -> x. e. ( ( ( J tX J ) CnP J ) ` <. L , ( F ` C ) >. ) )
214 73 46 75 75 10 78 195 208 213 limccnp2 
 |-  ( ph -> ( L x. ( F ` C ) ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) x. ( F ` C ) ) ) limCC C ) )
215 10 addcn 
 |-  + e. ( ( J tX J ) Cn J )
216 174 175 mulcld 
 |-  ( ph -> ( K x. ( G ` C ) ) e. CC )
217 210 45 mulcld 
 |-  ( ph -> ( L x. ( F ` C ) ) e. CC )
218 216 217 opelxpd 
 |-  ( ph -> <. ( K x. ( G ` C ) ) , ( L x. ( F ` C ) ) >. e. ( CC X. CC ) )
219 177 cncnpi 
 |-  ( ( + e. ( ( J tX J ) Cn J ) /\ <. ( K x. ( G ` C ) ) , ( L x. ( F ` C ) ) >. e. ( CC X. CC ) ) -> + e. ( ( ( J tX J ) CnP J ) ` <. ( K x. ( G ` C ) ) , ( L x. ( F ` C ) ) >. ) )
220 215 218 219 sylancr 
 |-  ( ph -> + e. ( ( ( J tX J ) CnP J ) ` <. ( K x. ( G ` C ) ) , ( L x. ( F ` C ) ) >. ) )
221 62 74 75 75 10 78 180 214 220 limccnp2 
 |-  ( ph -> ( ( K x. ( G ` C ) ) + ( L x. ( F ` C ) ) ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) x. ( G ` z ) ) + ( ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) x. ( F ` C ) ) ) ) limCC C ) )
222 44 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> C e. X )
223 34 222 ffvelrnd 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( F ` C ) e. CC )
224 39 223 subcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F ` z ) - ( F ` C ) ) e. CC )
225 224 61 mulcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) e. CC )
226 71 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> C e. Y )
227 58 226 ffvelrnd 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( G ` C ) e. CC )
228 61 227 subcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( G ` z ) - ( G ` C ) ) e. CC )
229 228 223 mulcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) e. CC )
230 49 222 sseldd 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> C e. CC )
231 50 230 subcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( z - C ) e. CC )
232 225 229 231 56 divdird 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) + ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) ) / ( z - C ) ) = ( ( ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) / ( z - C ) ) + ( ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) / ( z - C ) ) ) )
233 39 61 mulcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F ` z ) x. ( G ` z ) ) e. CC )
234 223 61 mulcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F ` C ) x. ( G ` z ) ) e. CC )
235 223 227 mulcld 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F ` C ) x. ( G ` C ) ) e. CC )
236 233 234 235 npncand 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F ` z ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` z ) ) ) + ( ( ( F ` C ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` C ) ) ) ) = ( ( ( F ` z ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` C ) ) ) )
237 39 223 61 subdird 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) = ( ( ( F ` z ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` z ) ) ) )
238 228 223 mulcomd 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) = ( ( F ` C ) x. ( ( G ` z ) - ( G ` C ) ) ) )
239 223 61 227 subdid 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F ` C ) x. ( ( G ` z ) - ( G ` C ) ) ) = ( ( ( F ` C ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` C ) ) ) )
240 238 239 eqtrd 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) = ( ( ( F ` C ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` C ) ) ) )
241 237 240 oveq12d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) + ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) ) = ( ( ( ( F ` z ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` z ) ) ) + ( ( ( F ` C ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` C ) ) ) ) )
242 1 ffnd 
 |-  ( ph -> F Fn X )
243 242 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> F Fn X )
244 3 ffnd 
 |-  ( ph -> G Fn Y )
245 244 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> G Fn Y )
246 ssexg 
 |-  ( ( X C_ CC /\ CC e. _V ) -> X e. _V )
247 48 102 246 sylancl 
 |-  ( ph -> X e. _V )
248 247 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> X e. _V )
249 ssexg 
 |-  ( ( Y C_ CC /\ CC e. _V ) -> Y e. _V )
250 66 102 249 sylancl 
 |-  ( ph -> Y e. _V )
251 250 adantr 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> Y e. _V )
252 eqid 
 |-  ( X i^i Y ) = ( X i^i Y )
253 eqidd 
 |-  ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ z e. X ) -> ( F ` z ) = ( F ` z ) )
254 eqidd 
 |-  ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ z e. Y ) -> ( G ` z ) = ( G ` z ) )
255 243 245 248 251 252 253 254 ofval 
 |-  ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ z e. ( X i^i Y ) ) -> ( ( F oF x. G ) ` z ) = ( ( F ` z ) x. ( G ` z ) ) )
256 37 255 mpdan 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F oF x. G ) ` z ) = ( ( F ` z ) x. ( G ` z ) ) )
257 eqidd 
 |-  ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ C e. X ) -> ( F ` C ) = ( F ` C ) )
258 eqidd 
 |-  ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ C e. Y ) -> ( G ` C ) = ( G ` C ) )
259 243 245 248 251 252 257 258 ofval 
 |-  ( ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) /\ C e. ( X i^i Y ) ) -> ( ( F oF x. G ) ` C ) = ( ( F ` C ) x. ( G ` C ) ) )
260 119 259 mpidan 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( F oF x. G ) ` C ) = ( ( F ` C ) x. ( G ` C ) ) )
261 256 260 oveq12d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) = ( ( ( F ` z ) x. ( G ` z ) ) - ( ( F ` C ) x. ( G ` C ) ) ) )
262 236 241 261 3eqtr4d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) + ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) ) = ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) )
263 262 oveq1d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) + ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) ) / ( z - C ) ) = ( ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) / ( z - C ) ) )
264 224 61 231 56 div23d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) / ( z - C ) ) = ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) x. ( G ` z ) ) )
265 228 223 231 56 div23d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) / ( z - C ) ) = ( ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) x. ( F ` C ) ) )
266 264 265 oveq12d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( ( F ` z ) - ( F ` C ) ) x. ( G ` z ) ) / ( z - C ) ) + ( ( ( ( G ` z ) - ( G ` C ) ) x. ( F ` C ) ) / ( z - C ) ) ) = ( ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) x. ( G ` z ) ) + ( ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) x. ( F ` C ) ) ) )
267 232 263 266 3eqtr3d 
 |-  ( ( ph /\ z e. ( ( X i^i Y ) \ { C } ) ) -> ( ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) / ( z - C ) ) = ( ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) x. ( G ` z ) ) + ( ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) x. ( F ` C ) ) ) )
268 267 mpteq2dva 
 |-  ( ph -> ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) / ( z - C ) ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) x. ( G ` z ) ) + ( ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) x. ( F ` C ) ) ) ) )
269 268 oveq1d 
 |-  ( ph -> ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) / ( z - C ) ) ) limCC C ) = ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( ( F ` z ) - ( F ` C ) ) / ( z - C ) ) x. ( G ` z ) ) + ( ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) x. ( F ` C ) ) ) ) limCC C ) )
270 221 269 eleqtrrd 
 |-  ( ph -> ( ( K x. ( G ` C ) ) + ( L x. ( F ` C ) ) ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) / ( z - C ) ) ) limCC C ) )
271 eqid 
 |-  ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) / ( z - C ) ) ) = ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) / ( z - C ) ) )
272 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
273 272 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
274 273 1 3 247 250 252 off 
 |-  ( ph -> ( F oF x. G ) : ( X i^i Y ) --> CC )
275 11 10 271 5 274 86 eldv 
 |-  ( ph -> ( C ( S _D ( F oF x. G ) ) ( ( K x. ( G ` C ) ) + ( L x. ( F ` C ) ) ) <-> ( C e. ( ( int ` ( J |`t S ) ) ` ( X i^i Y ) ) /\ ( ( K x. ( G ` C ) ) + ( L x. ( F ` C ) ) ) e. ( ( z e. ( ( X i^i Y ) \ { C } ) |-> ( ( ( ( F oF x. G ) ` z ) - ( ( F oF x. G ) ` C ) ) / ( z - C ) ) ) limCC C ) ) ) )
276 33 270 275 mpbir2and 
 |-  ( ph -> C ( S _D ( F oF x. G ) ) ( ( K x. ( G ` C ) ) + ( L x. ( F ` C ) ) ) )