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 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvco.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvco.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑋 )
dvco.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑇 )
dvcobr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
dvcobr.t ⊢ ( 𝜑 → 𝑇 ⊆ ℂ )
dvco.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
dvco.l ⊢ ( 𝜑 → 𝐿 ∈ 𝑉 )
dvco.bf ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ( 𝑆 D 𝐹 ) 𝐾 )
dvco.bg ⊢ ( 𝜑 → 𝐶 ( 𝑇 D 𝐺 ) 𝐿 )
dvco.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion dvcobr ( 𝜑 → 𝐶 ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ( 𝐾 · 𝐿 ) )

Proof

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