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