dvcobrOLD

Description: Obsolete version of dvcobr as of 10-Apr-2025. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvco.f	$⊢ φ \to F : X ⟶ ℂ$
	dvco.x	$⊢ φ \to X \subseteq S$
	dvco.g	$⊢ φ \to G : Y ⟶ X$
	dvco.y	$⊢ φ \to Y \subseteq T$
	dvcobr.s	$⊢ φ \to S \subseteq ℂ$
	dvcobr.t	$⊢ φ \to T \subseteq ℂ$
	dvco.bf	$⊢ φ \to G (C) F_{S}^{'} K$
	dvco.bg	$⊢ φ \to C G_{T}^{'} L$
	dvco.j	$⊢ J = TopOpen (ℂ_{fld})$
Assertion	dvcobrOLD	$⊢ φ \to C {(F \circ G)}_{T}^{'} K L$

Proof

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

Metamath Proof Explorer

Theorem dvcobrOLD

Proof