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

Proof

Step	Hyp	Ref	Expression
1		gg-dvco.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
2		gg-dvco.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
3		gg-dvco.g	⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑋 )
4		gg-dvco.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝑇 )
5		gg-dvcobr.s	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
6		gg-dvcobr.t	⊢ ( 𝜑 → 𝑇 ⊆ ℂ )
7		gg-dvco.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
8		gg-dvco.l	⊢ ( 𝜑 → 𝐿 ∈ 𝑉 )
9		gg-dvco.bf	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ( 𝑆 D 𝐹 ) 𝐾 )
10		gg-dvco.bg	⊢ ( 𝜑 → 𝐶 ( 𝑇 D 𝐺 ) 𝐿 )
11		gg-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		ffvelcdm	⊢ ( ( 𝐺 : 𝑌 ⟶ 𝑋 ∧ 𝑧 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑋 )
25	3 23 24	syl2an	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑋 )
26	22 25	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝐶 ) ∈ 𝑋 )
36	22 35	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
38	27 37	subcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ∈ ℂ )
39	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → 𝐺 : 𝑌 ⟶ ℂ )
40	23	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → 𝑧 ∈ 𝑌 )
41	39 40	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
42	33	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → 𝐶 ∈ 𝑌 )
43	39 42	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ 𝑋 )
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	gg-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	mpomulcn	⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×_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		df-mpt	⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) }
113	112	oveq1i	⊢ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) lim_ℂ 𝐶 ) = ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } lim_ℂ 𝐶 )
114	111 113	eleqtrdi	⊢ ( 𝜑 → ( 𝐾 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝐿 ) ∈ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } lim_ℂ 𝐶 ) )
115		ovmul	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝐾 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝐿 ) = ( 𝐾 · 𝐿 ) )
116	20 106 115	syl2anc	⊢ ( 𝜑 → ( 𝐾 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝐿 ) = ( 𝐾 · 𝐿 ) )
117		ovmul	⊢ ( ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ∈ ℂ ∧ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ ) → ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
118	50 52 117	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
119	118	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↔ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) )
120	119	pm5.32da	⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) ↔ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) ) )
121	120	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } )
122		df-mpt	⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) }
123	122	eqcomi	⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
124	123	eqeq2i	⊢ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } ↔ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) )
125	124	biimpi	⊢ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) )
126	125	oveq1d	⊢ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } lim_ℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) lim_ℂ 𝐶 ) )
127	121 126	syl	⊢ ( 𝜑 → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ 𝑤 = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) } lim_ℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) lim_ℂ 𝐶 ) )
128	114 116 127	3eltr3d	⊢ ( 𝜑 → ( 𝐾 · 𝐿 ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) lim_ℂ 𝐶 ) )
129		oveq1	⊢ ( 𝐾 = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) → ( 𝐾 · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
130	129	eqeq1d	⊢ ( 𝐾 = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) → ( ( 𝐾 · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) ↔ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) ) )
131		oveq1	⊢ ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) → ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
132	131	eqeq1d	⊢ ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) → ( ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) ↔ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) ) )
133	21	mul01d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐾 · 0 ) = 0 )
134	14	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑋 ⊆ ℂ )
135	134 25	sseldd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
136	134 35	sseldd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
137	135 136	subeq0ad	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) = 0 ↔ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) )
138	137	biimpar	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) = 0 )
139	138	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( 0 / ( 𝑧 − 𝐶 ) ) )
140	51	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑌 ⊆ ℂ )
141	23	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑧 ∈ 𝑌 )
142	140 141	sseldd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑧 ∈ ℂ )
143	140 34	sseldd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝐶 ∈ ℂ )
144	142 143	subcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ∈ ℂ )
145		eldifsni	⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) → 𝑧 ≠ 𝐶 )
146	145	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑧 ≠ 𝐶 )
147	142 143 146	subne0d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ≠ 0 )
148	144 147	div0d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 0 / ( 𝑧 − 𝐶 ) ) = 0 )
149	148	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 0 / ( 𝑧 − 𝐶 ) ) = 0 )
150	139 149	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = 0 )
151	150	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐾 · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝐾 · 0 ) )
152		fveq2	⊢ ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) )
153	26 36	subeq0ad	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) = 0 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) )
154	152 153	imbitrrid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) = 0 ) )
155	154	imp	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) = 0 )
156	155	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) = ( 0 / ( 𝑧 − 𝐶 ) ) )
157	156 149	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) = 0 )
158	133 151 157	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐾 · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
159	144	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝑧 − 𝐶 ) ∈ ℂ )
160	147	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝑧 − 𝐶 ) ≠ 0 )
161	38 44 159 48 160	dmdcan2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
162	130 132 158 161	ifbothda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
163		fvco3	⊢ ( ( 𝐺 : 𝑌 ⟶ 𝑋 ∧ 𝑧 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
164	3 23 163	syl2an	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
165	3 33	fvco3d	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) )
166	165	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) )
167	164 166	oveq12d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) )
168	167	oveq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
169	162 168	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
170	169	mpteq2dva	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
171	170	oveq1d	⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) lim_ℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) lim_ℂ 𝐶 ) )
172	128 171	eleqtrd	⊢ ( 𝜑 → ( 𝐾 · 𝐿 ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) lim_ℂ 𝐶 ) )
173		eqid	⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
174	1 3	fcod	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝑌 ⟶ ℂ )
175	12 11 173 6 174 4	eldv	⊢ ( 𝜑 → ( 𝐶 ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ( 𝐾 · 𝐿 ) ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾_t 𝑇 ) ) ‘ 𝑌 ) ∧ ( 𝐾 · 𝐿 ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) lim_ℂ 𝐶 ) ) ) )
176	18 172 175	mpbir2and	⊢ ( 𝜑 → 𝐶 ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ( 𝐾 · 𝐿 ) )

Metamath Proof Explorer

Theorem gg-dvcobr

Proof