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	$⊢ φ \to F : X ⟶ ℂ$
	gg-dvco.x	$⊢ φ \to X \subseteq S$
	gg-dvco.g	$⊢ φ \to G : Y ⟶ X$
	gg-dvco.y	$⊢ φ \to Y \subseteq T$
	gg-dvcobr.s	$⊢ φ \to S \subseteq ℂ$
	gg-dvcobr.t	$⊢ φ \to T \subseteq ℂ$
	gg-dvco.k	$⊢ φ \to K \in V$
	gg-dvco.l	$⊢ φ \to L \in V$
	gg-dvco.bf	$⊢ φ \to G (C) F_{S}^{'} K$
	gg-dvco.bg	$⊢ φ \to C G_{T}^{'} L$
	gg-dvco.j	$⊢ J = TopOpen (ℂ_{fld})$
Assertion	gg-dvcobr	$⊢ φ \to C {(F \circ G)}_{T}^{'} K L$

Proof

Step	Hyp	Ref	Expression
1		gg-dvco.f	$⊢ φ \to F : X ⟶ ℂ$
2		gg-dvco.x	$⊢ φ \to X \subseteq S$
3		gg-dvco.g	$⊢ φ \to G : Y ⟶ X$
4		gg-dvco.y	$⊢ φ \to Y \subseteq T$
5		gg-dvcobr.s	$⊢ φ \to S \subseteq ℂ$
6		gg-dvcobr.t	$⊢ φ \to T \subseteq ℂ$
7		gg-dvco.k	$⊢ φ \to K \in V$
8		gg-dvco.l	$⊢ φ \to L \in V$
9		gg-dvco.bf	$⊢ φ \to G (C) F_{S}^{'} K$
10		gg-dvco.bg	$⊢ φ \to C G_{T}^{'} L$
11		gg-dvco.j	$⊢ J = TopOpen (ℂ_{fld})$
12		eqid	$⊢ J ↾_{𝑡} T = J ↾_{𝑡} T$
13		eqid	$⊢ (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) = (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
14	2 5	sstrd	$⊢ φ \to X \subseteq ℂ$
15	3 14	fssd	$⊢ φ \to G : Y ⟶ ℂ$
16	12 11 13 6 15 4	eldv	$⊢ φ \to (C G_{T}^{'} L \leftrightarrow (C \in int (J ↾_{𝑡} T) (Y) \land L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)))$
17	10 16	mpbid	$⊢ φ \to (C \in int (J ↾_{𝑡} T) (Y) \land L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C))$
18	17	simpld	$⊢ φ \to C \in int (J ↾_{𝑡} T) (Y)$
19	5 1 2	dvcl	$⊢ (φ \land G (C) F_{S}^{'} K) \to K \in ℂ$
20	9 19	mpdan	$⊢ φ \to K \in ℂ$
21	20	ad2antrr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to K \in ℂ$
22	1	adantr	$⊢ (φ \land z \in (Y ∖ \{C\})) \to F : X ⟶ ℂ$
23		eldifi	$⊢ z \in (Y ∖ \{C\}) \to z \in Y$
24		ffvelcdm	$⊢ (G : Y ⟶ X \land z \in Y) \to G (z) \in X$
25	3 23 24	syl2an	$⊢ (φ \land z \in (Y ∖ \{C\})) \to G (z) \in X$
26	22 25	ffvelcdmd	$⊢ (φ \land z \in (Y ∖ \{C\})) \to F (G (z)) \in ℂ$
27	26	adantr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to F (G (z)) \in ℂ$
28	3	adantr	$⊢ (φ \land z \in (Y ∖ \{C\})) \to G : Y ⟶ X$
29	6 15 4	dvbss	$⊢ φ \to dom G_{T}^{'} \subseteq Y$
30		reldv	$⊢ Rel G_{T}^{'}$
31		releldm	$⊢ (Rel G_{T}^{'} \land C G_{T}^{'} L) \to C \in dom G_{T}^{'}$
32	30 10 31	sylancr	$⊢ φ \to C \in dom G_{T}^{'}$
33	29 32	sseldd	$⊢ φ \to C \in Y$
34	33	adantr	$⊢ (φ \land z \in (Y ∖ \{C\})) \to C \in Y$
35	28 34	ffvelcdmd	$⊢ (φ \land z \in (Y ∖ \{C\})) \to G (C) \in X$
36	22 35	ffvelcdmd	$⊢ (φ \land z \in (Y ∖ \{C\})) \to F (G (C)) \in ℂ$
37	36	adantr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to F (G (C)) \in ℂ$
38	27 37	subcld	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to F (G (z)) - F (G (C)) \in ℂ$
39	15	ad2antrr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to G : Y ⟶ ℂ$
40	23	ad2antlr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to z \in Y$
41	39 40	ffvelcdmd	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to G (z) \in ℂ$
42	33	ad2antrr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to C \in Y$
43	39 42	ffvelcdmd	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to G (C) \in ℂ$
44	41 43	subcld	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to G (z) - G (C) \in ℂ$
45		simpr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to \neg G (z) = G (C)$
46	41 43	subeq0ad	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to (G (z) - G (C) = 0 \leftrightarrow G (z) = G (C))$
47	46	necon3abid	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to (G (z) - G (C) \neq 0 \leftrightarrow \neg G (z) = G (C))$
48	45 47	mpbird	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to G (z) - G (C) \neq 0$
49	38 44 48	divcld	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to \frac{F (G (z)) - F (G (C))}{G (z) - G (C)} \in ℂ$
50	21 49	ifclda	$⊢ (φ \land z \in (Y ∖ \{C\})) \to if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) \in ℂ$
51	4 6	sstrd	$⊢ φ \to Y \subseteq ℂ$
52	15 51 33	dvlem	$⊢ (φ \land z \in (Y ∖ \{C\})) \to \frac{G (z) - G (C)}{z - C} \in ℂ$
53		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
54	11	cnfldtopon	$⊢ J \in TopOn (ℂ)$
55		txtopon	$⊢ (J \in TopOn (ℂ) \land J \in TopOn (ℂ)) \to J \times_{t} J \in TopOn (ℂ \times ℂ)$
56	54 54 55	mp2an	$⊢ J \times_{t} J \in TopOn (ℂ \times ℂ)$
57	56	toponrestid	$⊢ J \times_{t} J = (J \times_{t} J) ↾_{𝑡} (ℂ \times ℂ)$
58	25	anim1i	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) \neq G (C)) \to (G (z) \in X \land G (z) \neq G (C))$
59		eldifsn	$⊢ G (z) \in (X ∖ \{G (C)\}) \leftrightarrow (G (z) \in X \land G (z) \neq G (C))$
60	58 59	sylibr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) \neq G (C)) \to G (z) \in (X ∖ \{G (C)\})$
61	60	anasss	$⊢ (φ \land (z \in (Y ∖ \{C\}) \land G (z) \neq G (C))) \to G (z) \in (X ∖ \{G (C)\})$
62		eldifsni	$⊢ y \in (X ∖ \{G (C)\}) \to y \neq G (C)$
63		ifnefalse	$⊢ y \neq G (C) \to if (y = G (C), K, \frac{F (y) - F (G (C))}{y - G (C)}) = \frac{F (y) - F (G (C))}{y - G (C)}$
64	62 63	syl	$⊢ y \in (X ∖ \{G (C)\}) \to if (y = G (C), K, \frac{F (y) - F (G (C))}{y - G (C)}) = \frac{F (y) - F (G (C))}{y - G (C)}$
65	64	adantl	$⊢ (φ \land y \in (X ∖ \{G (C)\})) \to if (y = G (C), K, \frac{F (y) - F (G (C))}{y - G (C)}) = \frac{F (y) - F (G (C))}{y - G (C)}$
66	3 33	ffvelcdmd	$⊢ φ \to G (C) \in X$
67	1 14 66	dvlem	$⊢ (φ \land y \in (X ∖ \{G (C)\})) \to \frac{F (y) - F (G (C))}{y - G (C)} \in ℂ$
68	65 67	eqeltrd	$⊢ (φ \land y \in (X ∖ \{G (C)\})) \to if (y = G (C), K, \frac{F (y) - F (G (C))}{y - G (C)}) \in ℂ$
69		limcresi	$⊢ G {lim}_{ℂ} C \subseteq ({G ↾}_{(Y ∖ \{C\})}) {lim}_{ℂ} C$
70	3	feqmptd	$⊢ φ \to G = (z \in Y ⟼ G (z))$
71	70	reseq1d	$⊢ φ \to {G ↾}_{(Y ∖ \{C\})} = {(z \in Y ⟼ G (z)) ↾}_{(Y ∖ \{C\})}$
72		difss	$⊢ Y ∖ \{C\} \subseteq Y$
73		resmpt	$⊢ Y ∖ \{C\} \subseteq Y \to {(z \in Y ⟼ G (z)) ↾}_{(Y ∖ \{C\})} = (z \in (Y ∖ \{C\}) ⟼ G (z))$
74	72 73	ax-mp	$⊢ {(z \in Y ⟼ G (z)) ↾}_{(Y ∖ \{C\})} = (z \in (Y ∖ \{C\}) ⟼ G (z))$
75	71 74	eqtrdi	$⊢ φ \to {G ↾}_{(Y ∖ \{C\})} = (z \in (Y ∖ \{C\}) ⟼ G (z))$
76	75	oveq1d	$⊢ φ \to ({G ↾}_{(Y ∖ \{C\})}) {lim}_{ℂ} C = (z \in (Y ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C$
77	69 76	sseqtrid	$⊢ φ \to G {lim}_{ℂ} C \subseteq (z \in (Y ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C$
78		eqid	$⊢ J ↾_{𝑡} Y = J ↾_{𝑡} Y$
79	78 11	gg-dvcnp2	$⊢ ((T \subseteq ℂ \land G : Y ⟶ ℂ \land Y \subseteq T) \land C \in dom G_{T}^{'}) \to G \in ((J ↾_{𝑡} Y) CnP J) (C)$
80	6 15 4 32 79	syl31anc	$⊢ φ \to G \in ((J ↾_{𝑡} Y) CnP J) (C)$
81	11 78	cnplimc	$⊢ (Y \subseteq ℂ \land C \in Y) \to (G \in ((J ↾_{𝑡} Y) CnP J) (C) \leftrightarrow (G : Y ⟶ ℂ \land G (C) \in (G {lim}_{ℂ} C)))$
82	51 33 81	syl2anc	$⊢ φ \to (G \in ((J ↾_{𝑡} Y) CnP J) (C) \leftrightarrow (G : Y ⟶ ℂ \land G (C) \in (G {lim}_{ℂ} C)))$
83	80 82	mpbid	$⊢ φ \to (G : Y ⟶ ℂ \land G (C) \in (G {lim}_{ℂ} C))$
84	83	simprd	$⊢ φ \to G (C) \in (G {lim}_{ℂ} C)$
85	77 84	sseldd	$⊢ φ \to G (C) \in ((z \in (Y ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C)$
86		eqid	$⊢ J ↾_{𝑡} S = J ↾_{𝑡} S$
87		eqid	$⊢ (y \in (X ∖ \{G (C)\}) ⟼ \frac{F (y) - F (G (C))}{y - G (C)}) = (y \in (X ∖ \{G (C)\}) ⟼ \frac{F (y) - F (G (C))}{y - G (C)})$
88	86 11 87 5 1 2	eldv	$⊢ φ \to (G (C) F_{S}^{'} K \leftrightarrow (G (C) \in int (J ↾_{𝑡} S) (X) \land K \in ((y \in (X ∖ \{G (C)\}) ⟼ \frac{F (y) - F (G (C))}{y - G (C)}) {lim}_{ℂ} G (C))))$
89	9 88	mpbid	$⊢ φ \to (G (C) \in int (J ↾_{𝑡} S) (X) \land K \in ((y \in (X ∖ \{G (C)\}) ⟼ \frac{F (y) - F (G (C))}{y - G (C)}) {lim}_{ℂ} G (C)))$
90	89	simprd	$⊢ φ \to K \in ((y \in (X ∖ \{G (C)\}) ⟼ \frac{F (y) - F (G (C))}{y - G (C)}) {lim}_{ℂ} G (C))$
91	64	mpteq2ia	$⊢ (y \in (X ∖ \{G (C)\}) ⟼ if (y = G (C), K, \frac{F (y) - F (G (C))}{y - G (C)})) = (y \in (X ∖ \{G (C)\}) ⟼ \frac{F (y) - F (G (C))}{y - G (C)})$
92	91	oveq1i	$⊢ (y \in (X ∖ \{G (C)\}) ⟼ if (y = G (C), K, \frac{F (y) - F (G (C))}{y - G (C)})) {lim}_{ℂ} G (C) = (y \in (X ∖ \{G (C)\}) ⟼ \frac{F (y) - F (G (C))}{y - G (C)}) {lim}_{ℂ} G (C)$
93	90 92	eleqtrrdi	$⊢ φ \to K \in ((y \in (X ∖ \{G (C)\}) ⟼ if (y = G (C), K, \frac{F (y) - F (G (C))}{y - G (C)})) {lim}_{ℂ} G (C))$
94		eqeq1	$⊢ y = G (z) \to (y = G (C) \leftrightarrow G (z) = G (C))$
95		fveq2	$⊢ y = G (z) \to F (y) = F (G (z))$
96	95	oveq1d	$⊢ y = G (z) \to F (y) - F (G (C)) = F (G (z)) - F (G (C))$
97		oveq1	$⊢ y = G (z) \to y - G (C) = G (z) - G (C)$
98	96 97	oveq12d	$⊢ y = G (z) \to \frac{F (y) - F (G (C))}{y - G (C)} = \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}$
99	94 98	ifbieq2d	$⊢ y = G (z) \to if (y = G (C), K, \frac{F (y) - F (G (C))}{y - G (C)}) = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)})$
100		iftrue	$⊢ G (z) = G (C) \to if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) = K$
101	100	ad2antll	$⊢ (φ \land (z \in (Y ∖ \{C\}) \land G (z) = G (C))) \to if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) = K$
102	61 68 85 93 99 101	limcco	$⊢ φ \to K \in ((z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)})) {lim}_{ℂ} C)$
103	17	simprd	$⊢ φ \to L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)$
104	11	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
105	6 15 4	dvcl	$⊢ (φ \land C G_{T}^{'} L) \to L \in ℂ$
106	10 105	mpdan	$⊢ φ \to L \in ℂ$
107	20 106	opelxpd	$⊢ φ \to ⟨K, L⟩ \in (ℂ \times ℂ)$
108	56	toponunii	$⊢ ℂ \times ℂ = ⋃ (J \times_{t} J)$
109	108	cncnpi	$⊢ ((u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J) \land ⟨K, L⟩ \in (ℂ \times ℂ)) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) CnP J) (⟨K, L⟩)$
110	104 107 109	sylancr	$⊢ φ \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) CnP J) (⟨K, L⟩)$
111	50 52 53 53 11 57 102 103 110	limccnp2	$⊢ φ \to K (u \in ℂ, v \in ℂ ⟼ u v) L \in ((z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C})) {lim}_{ℂ} C)$
112		df-mpt	$⊢ (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C})) = \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\}$
113	112	oveq1i	$⊢ (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C})) {lim}_{ℂ} C = \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} {lim}_{ℂ} C$
114	111 113	eleqtrdi	$⊢ φ \to K (u \in ℂ, v \in ℂ ⟼ u v) L \in (\{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} {lim}_{ℂ} C)$
115		ovmul	$⊢ (K \in ℂ \land L \in ℂ) \to K (u \in ℂ, v \in ℂ ⟼ u v) L = K L$
116	20 106 115	syl2anc	$⊢ φ \to K (u \in ℂ, v \in ℂ ⟼ u v) L = K L$
117		ovmul	$⊢ (if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) \in ℂ \land \frac{G (z) - G (C)}{z - C} \in ℂ) \to if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}) = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})$
118	50 52 117	syl2anc	$⊢ (φ \land z \in (Y ∖ \{C\})) \to if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}) = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})$
119	118	eqeq2d	$⊢ (φ \land z \in (Y ∖ \{C\})) \to (w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}) \leftrightarrow w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))$
120	119	pm5.32da	$⊢ φ \to ((z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C})) \leftrightarrow (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})))$
121	120	opabbidv	$⊢ φ \to \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} = \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))\}$
122		df-mpt	$⊢ (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})) = \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))\}$
123	122	eqcomi	$⊢ \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))\} = (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))$
124	123	eqeq2i	$⊢ \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} = \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))\} \leftrightarrow \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} = (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))$
125	124	biimpi	$⊢ \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} = \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))\} \to \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} = (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))$
126	125	oveq1d	$⊢ \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} = \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}))\} \to \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} {lim}_{ℂ} C = (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})) {lim}_{ℂ} C$
127	121 126	syl	$⊢ φ \to \{⟨z, w⟩ \| (z \in (Y ∖ \{C\}) \land w = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (u \in ℂ, v \in ℂ ⟼ u v) (\frac{G (z) - G (C)}{z - C}))\} {lim}_{ℂ} C = (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})) {lim}_{ℂ} C$
128	114 116 127	3eltr3d	$⊢ φ \to K L \in ((z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})) {lim}_{ℂ} C)$
129		oveq1	$⊢ K = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) \to K (\frac{G (z) - G (C)}{z - C}) = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})$
130	129	eqeq1d	$⊢ K = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) \to (K (\frac{G (z) - G (C)}{z - C}) = \frac{F (G (z)) - F (G (C))}{z - C} \leftrightarrow if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}) = \frac{F (G (z)) - F (G (C))}{z - C})$
131		oveq1	$⊢ \frac{F (G (z)) - F (G (C))}{G (z) - G (C)} = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) \to (\frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}) = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})$
132	131	eqeq1d	$⊢ \frac{F (G (z)) - F (G (C))}{G (z) - G (C)} = if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) \to ((\frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}) = \frac{F (G (z)) - F (G (C))}{z - C} \leftrightarrow if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}) = \frac{F (G (z)) - F (G (C))}{z - C})$
133	21	mul01d	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to K \cdot 0 = 0$
134	14	adantr	$⊢ (φ \land z \in (Y ∖ \{C\})) \to X \subseteq ℂ$
135	134 25	sseldd	$⊢ (φ \land z \in (Y ∖ \{C\})) \to G (z) \in ℂ$
136	134 35	sseldd	$⊢ (φ \land z \in (Y ∖ \{C\})) \to G (C) \in ℂ$
137	135 136	subeq0ad	$⊢ (φ \land z \in (Y ∖ \{C\})) \to (G (z) - G (C) = 0 \leftrightarrow G (z) = G (C))$
138	137	biimpar	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to G (z) - G (C) = 0$
139	138	oveq1d	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to \frac{G (z) - G (C)}{z - C} = \frac{0}{z - C}$
140	51	adantr	$⊢ (φ \land z \in (Y ∖ \{C\})) \to Y \subseteq ℂ$
141	23	adantl	$⊢ (φ \land z \in (Y ∖ \{C\})) \to z \in Y$
142	140 141	sseldd	$⊢ (φ \land z \in (Y ∖ \{C\})) \to z \in ℂ$
143	140 34	sseldd	$⊢ (φ \land z \in (Y ∖ \{C\})) \to C \in ℂ$
144	142 143	subcld	$⊢ (φ \land z \in (Y ∖ \{C\})) \to z - C \in ℂ$
145		eldifsni	$⊢ z \in (Y ∖ \{C\}) \to z \neq C$
146	145	adantl	$⊢ (φ \land z \in (Y ∖ \{C\})) \to z \neq C$
147	142 143 146	subne0d	$⊢ (φ \land z \in (Y ∖ \{C\})) \to z - C \neq 0$
148	144 147	div0d	$⊢ (φ \land z \in (Y ∖ \{C\})) \to \frac{0}{z - C} = 0$
149	148	adantr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to \frac{0}{z - C} = 0$
150	139 149	eqtrd	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to \frac{G (z) - G (C)}{z - C} = 0$
151	150	oveq2d	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to K (\frac{G (z) - G (C)}{z - C}) = K \cdot 0$
152		fveq2	$⊢ G (z) = G (C) \to F (G (z)) = F (G (C))$
153	26 36	subeq0ad	$⊢ (φ \land z \in (Y ∖ \{C\})) \to (F (G (z)) - F (G (C)) = 0 \leftrightarrow F (G (z)) = F (G (C)))$
154	152 153	imbitrrid	$⊢ (φ \land z \in (Y ∖ \{C\})) \to (G (z) = G (C) \to F (G (z)) - F (G (C)) = 0)$
155	154	imp	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to F (G (z)) - F (G (C)) = 0$
156	155	oveq1d	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to \frac{F (G (z)) - F (G (C))}{z - C} = \frac{0}{z - C}$
157	156 149	eqtrd	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to \frac{F (G (z)) - F (G (C))}{z - C} = 0$
158	133 151 157	3eqtr4d	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land G (z) = G (C)) \to K (\frac{G (z) - G (C)}{z - C}) = \frac{F (G (z)) - F (G (C))}{z - C}$
159	144	adantr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to z - C \in ℂ$
160	147	adantr	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to z - C \neq 0$
161	38 44 159 48 160	dmdcan2d	$⊢ ((φ \land z \in (Y ∖ \{C\})) \land \neg G (z) = G (C)) \to (\frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}) = \frac{F (G (z)) - F (G (C))}{z - C}$
162	130 132 158 161	ifbothda	$⊢ (φ \land z \in (Y ∖ \{C\})) \to if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}) = \frac{F (G (z)) - F (G (C))}{z - C}$
163		fvco3	$⊢ (G : Y ⟶ X \land z \in Y) \to (F \circ G) (z) = F (G (z))$
164	3 23 163	syl2an	$⊢ (φ \land z \in (Y ∖ \{C\})) \to (F \circ G) (z) = F (G (z))$
165	3 33	fvco3d	$⊢ φ \to (F \circ G) (C) = F (G (C))$
166	165	adantr	$⊢ (φ \land z \in (Y ∖ \{C\})) \to (F \circ G) (C) = F (G (C))$
167	164 166	oveq12d	$⊢ (φ \land z \in (Y ∖ \{C\})) \to (F \circ G) (z) - (F \circ G) (C) = F (G (z)) - F (G (C))$
168	167	oveq1d	$⊢ (φ \land z \in (Y ∖ \{C\})) \to \frac{(F \circ G) (z) - (F \circ G) (C)}{z - C} = \frac{F (G (z)) - F (G (C))}{z - C}$
169	162 168	eqtr4d	$⊢ (φ \land z \in (Y ∖ \{C\})) \to if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C}) = \frac{(F \circ G) (z) - (F \circ G) (C)}{z - C}$
170	169	mpteq2dva	$⊢ φ \to (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})) = (z \in (Y ∖ \{C\}) ⟼ \frac{(F \circ G) (z) - (F \circ G) (C)}{z - C})$
171	170	oveq1d	$⊢ φ \to (z \in (Y ∖ \{C\}) ⟼ if (G (z) = G (C), K, \frac{F (G (z)) - F (G (C))}{G (z) - G (C)}) (\frac{G (z) - G (C)}{z - C})) {lim}_{ℂ} C = (z \in (Y ∖ \{C\}) ⟼ \frac{(F \circ G) (z) - (F \circ G) (C)}{z - C}) {lim}_{ℂ} C$
172	128 171	eleqtrd	$⊢ φ \to K L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{(F \circ G) (z) - (F \circ G) (C)}{z - C}) {lim}_{ℂ} C)$
173		eqid	$⊢ (z \in (Y ∖ \{C\}) ⟼ \frac{(F \circ G) (z) - (F \circ G) (C)}{z - C}) = (z \in (Y ∖ \{C\}) ⟼ \frac{(F \circ G) (z) - (F \circ G) (C)}{z - C})$
174	1 3	fcod	$⊢ φ \to (F \circ G) : Y ⟶ ℂ$
175	12 11 173 6 174 4	eldv	$⊢ φ \to (C {(F \circ G)}_{T}^{'} K L \leftrightarrow (C \in int (J ↾_{𝑡} T) (Y) \land K L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{(F \circ G) (z) - (F \circ G) (C)}{z - C}) {lim}_{ℂ} C)))$
176	18 172 175	mpbir2and	$⊢ φ \to C {(F \circ G)}_{T}^{'} K L$

Metamath Proof Explorer

Theorem gg-dvcobr

Proof