dvmulbr

Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	dvadd.f	$⊢ φ \to F : X ⟶ ℂ$
	dvadd.x	$⊢ φ \to X \subseteq S$
	dvadd.g	$⊢ φ \to G : Y ⟶ ℂ$
	dvadd.y	$⊢ φ \to Y \subseteq S$
	dvaddbr.s	$⊢ φ \to S \subseteq ℂ$
	dvadd.k	$⊢ φ \to K \in V$
	dvadd.l	$⊢ φ \to L \in V$
	dvadd.bf	$⊢ φ \to C F_{S}^{'} K$
	dvadd.bg	$⊢ φ \to C G_{S}^{'} L$
	dvadd.j	$⊢ J = TopOpen (ℂ_{fld})$
Assertion	dvmulbr	$⊢ φ \to C {(F \times_{f} G)}_{S}^{'} (K G (C) + L F (C))$

Proof

Step	Hyp	Ref	Expression
1		dvadd.f	$⊢ φ \to F : X ⟶ ℂ$
2		dvadd.x	$⊢ φ \to X \subseteq S$
3		dvadd.g	$⊢ φ \to G : Y ⟶ ℂ$
4		dvadd.y	$⊢ φ \to Y \subseteq S$
5		dvaddbr.s	$⊢ φ \to S \subseteq ℂ$
6		dvadd.k	$⊢ φ \to K \in V$
7		dvadd.l	$⊢ φ \to L \in V$
8		dvadd.bf	$⊢ φ \to C F_{S}^{'} K$
9		dvadd.bg	$⊢ φ \to C G_{S}^{'} L$
10		dvadd.j	$⊢ J = TopOpen (ℂ_{fld})$
11		eqid	$⊢ J ↾_{𝑡} S = J ↾_{𝑡} S$
12		eqid	$⊢ (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) = (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C})$
13	11 10 12 5 1 2	eldv	$⊢ φ \to (C F_{S}^{'} K \leftrightarrow (C \in int (J ↾_{𝑡} S) (X) \land K \in ((z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C)))$
14	8 13	mpbid	$⊢ φ \to (C \in int (J ↾_{𝑡} S) (X) \land K \in ((z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C))$
15	14	simpld	$⊢ φ \to C \in int (J ↾_{𝑡} S) (X)$
16		eqid	$⊢ (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) = (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
17	11 10 16 5 3 4	eldv	$⊢ φ \to (C G_{S}^{'} L \leftrightarrow (C \in int (J ↾_{𝑡} S) (Y) \land L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)))$
18	9 17	mpbid	$⊢ φ \to (C \in int (J ↾_{𝑡} S) (Y) \land L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C))$
19	18	simpld	$⊢ φ \to C \in int (J ↾_{𝑡} S) (Y)$
20	15 19	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) (X) \cap int (J ↾_{𝑡} S) (Y))$
21	10	cnfldtopon	$⊢ J \in TopOn (ℂ)$
22		resttopon	$⊢ (J \in TopOn (ℂ) \land S \subseteq ℂ) \to J ↾_{𝑡} S \in TopOn (S)$
23	21 5 22	sylancr	$⊢ φ \to J ↾_{𝑡} S \in TopOn (S)$
24		topontop	$⊢ J ↾_{𝑡} S \in TopOn (S) \to J ↾_{𝑡} S \in Top$
25	23 24	syl	$⊢ φ \to J ↾_{𝑡} S \in Top$
26		toponuni	$⊢ J ↾_{𝑡} S \in TopOn (S) \to S = ⋃ (J ↾_{𝑡} S)$
27	23 26	syl	$⊢ φ \to S = ⋃ (J ↾_{𝑡} S)$
28	2 27	sseqtrd	$⊢ φ \to X \subseteq ⋃ (J ↾_{𝑡} S)$
29	4 27	sseqtrd	$⊢ φ \to Y \subseteq ⋃ (J ↾_{𝑡} S)$
30		eqid	$⊢ ⋃ (J ↾_{𝑡} S) = ⋃ (J ↾_{𝑡} S)$
31	30	ntrin	$⊢ (J ↾_{𝑡} S \in Top \land X \subseteq ⋃ (J ↾_{𝑡} S) \land Y \subseteq ⋃ (J ↾_{𝑡} S)) \to int (J ↾_{𝑡} S) (X \cap Y) = int (J ↾_{𝑡} S) (X) \cap int (J ↾_{𝑡} S) (Y)$
32	25 28 29 31	syl3anc	$⊢ φ \to int (J ↾_{𝑡} S) (X \cap Y) = int (J ↾_{𝑡} S) (X) \cap int (J ↾_{𝑡} S) (Y)$
33	20 32	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} S) (X \cap Y)$
34	1	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F : X ⟶ ℂ$
35		inss1	$⊢ X \cap Y \subseteq X$
36		eldifi	$⊢ z \in ((X \cap Y) ∖ \{C\}) \to z \in (X \cap Y)$
37	36	adantl	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in (X \cap Y)$
38	35 37	sselid	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in X$
39	34 38	ffvelrnd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) \in ℂ$
40	5 1 2	dvbss	$⊢ φ \to dom F_{S}^{'} \subseteq X$
41		reldv	$⊢ Rel F_{S}^{'}$
42		releldm	$⊢ (Rel F_{S}^{'} \land C F_{S}^{'} K) \to C \in dom F_{S}^{'}$
43	41 8 42	sylancr	$⊢ φ \to C \in dom F_{S}^{'}$
44	40 43	sseldd	$⊢ φ \to C \in X$
45	1 44	ffvelrnd	$⊢ φ \to F (C) \in ℂ$
46	45	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) \in ℂ$
47	39 46	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) - F (C) \in ℂ$
48	2 5	sstrd	$⊢ φ \to X \subseteq ℂ$
49	48	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to X \subseteq ℂ$
50	49 38	sseldd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in ℂ$
51	48 44	sseldd	$⊢ φ \to C \in ℂ$
52	51	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in ℂ$
53	50 52	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z - C \in ℂ$
54		eldifsni	$⊢ z \in ((X \cap Y) ∖ \{C\}) \to z \neq C$
55	54	adantl	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \neq C$
56	50 52 55	subne0d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z - C \neq 0$
57	47 53 56	divcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{F (z) - F (C)}{z - C} \in ℂ$
58	3	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G : Y ⟶ ℂ$
59		inss2	$⊢ X \cap Y \subseteq Y$
60	59 37	sselid	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in Y$
61	58 60	ffvelrnd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (z) \in ℂ$
62	57 61	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (\frac{F (z) - F (C)}{z - C}) G (z) \in ℂ$
63		ssdif	$⊢ X \cap Y \subseteq Y \to (X \cap Y) ∖ \{C\} \subseteq Y ∖ \{C\}$
64	59 63	mp1i	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq Y ∖ \{C\}$
65	64	sselda	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in (Y ∖ \{C\})$
66	4 5	sstrd	$⊢ φ \to Y \subseteq ℂ$
67	5 3 4	dvbss	$⊢ φ \to dom G_{S}^{'} \subseteq Y$
68		reldv	$⊢ Rel G_{S}^{'}$
69		releldm	$⊢ (Rel G_{S}^{'} \land C G_{S}^{'} L) \to C \in dom G_{S}^{'}$
70	68 9 69	sylancr	$⊢ φ \to C \in dom G_{S}^{'}$
71	67 70	sseldd	$⊢ φ \to C \in Y$
72	3 66 71	dvlem	$⊢ (φ \land z \in (Y ∖ \{C\})) \to \frac{G (z) - G (C)}{z - C} \in ℂ$
73	65 72	syldan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{G (z) - G (C)}{z - C} \in ℂ$
74	73 46	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (\frac{G (z) - G (C)}{z - C}) F (C) \in ℂ$
75		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
76		txtopon	$⊢ (J \in TopOn (ℂ) \land J \in TopOn (ℂ)) \to J \times_{t} J \in TopOn (ℂ \times ℂ)$
77	21 21 76	mp2an	$⊢ J \times_{t} J \in TopOn (ℂ \times ℂ)$
78	77	toponrestid	$⊢ J \times_{t} J = (J \times_{t} J) ↾_{𝑡} (ℂ \times ℂ)$
79	14	simprd	$⊢ φ \to K \in ((z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C)$
80	1 48 44	dvlem	$⊢ (φ \land z \in (X ∖ \{C\})) \to \frac{F (z) - F (C)}{z - C} \in ℂ$
81	80	fmpttd	$⊢ φ \to (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) : X ∖ \{C\} ⟶ ℂ$
82		ssdif	$⊢ X \cap Y \subseteq X \to (X \cap Y) ∖ \{C\} \subseteq X ∖ \{C\}$
83	35 82	mp1i	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq X ∖ \{C\}$
84	48	ssdifssd	$⊢ φ \to X ∖ \{C\} \subseteq ℂ$
85		eqid	$⊢ J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})$
86	35 2	sstrid	$⊢ φ \to X \cap Y \subseteq S$
87	86 27	sseqtrd	$⊢ φ \to X \cap Y \subseteq ⋃ (J ↾_{𝑡} S)$
88		difssd	$⊢ φ \to ⋃ (J ↾_{𝑡} S) ∖ X \subseteq ⋃ (J ↾_{𝑡} S)$
89	87 88	unssd	$⊢ φ \to (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X) \subseteq ⋃ (J ↾_{𝑡} S)$
90		ssun1	$⊢ X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)$
91	90	a1i	$⊢ φ \to X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)$
92	30	ntrss	$⊢ (J ↾_{𝑡} S \in Top \land (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X) \subseteq ⋃ (J ↾_{𝑡} S) \land X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X))$
93	25 89 91 92	syl3anc	$⊢ φ \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X))$
94	93 33	sseldd	$⊢ φ \to C \in int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X))$
95	94 44	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X)$
96	35	a1i	$⊢ φ \to X \cap Y \subseteq X$
97		eqid	$⊢ (J ↾_{𝑡} S) ↾_{𝑡} X = (J ↾_{𝑡} S) ↾_{𝑡} X$
98	30 97	restntr	$⊢ (J ↾_{𝑡} S \in Top \land X \subseteq ⋃ (J ↾_{𝑡} S) \land X \cap Y \subseteq X) \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X$
99	25 28 96 98	syl3anc	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X$
100	10	cnfldtop	$⊢ J \in Top$
101	100	a1i	$⊢ φ \to J \in Top$
102		cnex	$⊢ ℂ \in V$
103		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
104	5 102 103	sylancl	$⊢ φ \to S \in V$
105		restabs	$⊢ (J \in Top \land X \subseteq S \land S \in V) \to (J ↾_{𝑡} S) ↾_{𝑡} X = J ↾_{𝑡} X$
106	101 2 104 105	syl3anc	$⊢ φ \to (J ↾_{𝑡} S) ↾_{𝑡} X = J ↾_{𝑡} X$
107	106	fveq2d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) = int (J ↾_{𝑡} X)$
108	107	fveq1d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) (X \cap Y) = int (J ↾_{𝑡} X) (X \cap Y)$
109	99 108	eqtr3d	$⊢ φ \to int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X = int (J ↾_{𝑡} X) (X \cap Y)$
110	95 109	eleqtrd	$⊢ φ \to C \in int (J ↾_{𝑡} X) (X \cap Y)$
111		undif1	$⊢ (X ∖ \{C\}) \cup \{C\} = X \cup \{C\}$
112	44	snssd	$⊢ φ \to \{C\} \subseteq X$
113		ssequn2	$⊢ \{C\} \subseteq X \leftrightarrow X \cup \{C\} = X$
114	112 113	sylib	$⊢ φ \to X \cup \{C\} = X$
115	111 114	syl5eq	$⊢ φ \to (X ∖ \{C\}) \cup \{C\} = X$
116	115	oveq2d	$⊢ φ \to J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} X$
117	116	fveq2d	$⊢ φ \to int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) = int (J ↾_{𝑡} X)$
118		undif1	$⊢ ((X \cap Y) ∖ \{C\}) \cup \{C\} = (X \cap Y) \cup \{C\}$
119	44 71	elind	$⊢ φ \to C \in (X \cap Y)$
120	119	snssd	$⊢ φ \to \{C\} \subseteq X \cap Y$
121		ssequn2	$⊢ \{C\} \subseteq X \cap Y \leftrightarrow (X \cap Y) \cup \{C\} = X \cap Y$
122	120 121	sylib	$⊢ φ \to (X \cap Y) \cup \{C\} = X \cap Y$
123	118 122	syl5eq	$⊢ φ \to ((X \cap Y) ∖ \{C\}) \cup \{C\} = X \cap Y$
124	117 123	fveq12d	$⊢ φ \to int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\}) = int (J ↾_{𝑡} X) (X \cap Y)$
125	110 124	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\})$
126	81 83 84 10 85 125	limcres	$⊢ φ \to ({(z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C$
127	83	resmptd	$⊢ φ \to {(z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C})$
128	127	oveq1d	$⊢ φ \to ({(z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C$
129	126 128	eqtr3d	$⊢ φ \to (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C$
130	79 129	eleqtrd	$⊢ φ \to K \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C)$
131		eqid	$⊢ J ↾_{𝑡} Y = J ↾_{𝑡} Y$
132	131 10	dvcnp2	$⊢ ((S \subseteq ℂ \land G : Y ⟶ ℂ \land Y \subseteq S) \land C \in dom G_{S}^{'}) \to G \in ((J ↾_{𝑡} Y) CnP J) (C)$
133	5 3 4 70 132	syl31anc	$⊢ φ \to G \in ((J ↾_{𝑡} Y) CnP J) (C)$
134	10 131	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)))$
135	66 71 134	syl2anc	$⊢ φ \to (G \in ((J ↾_{𝑡} Y) CnP J) (C) \leftrightarrow (G : Y ⟶ ℂ \land G (C) \in (G {lim}_{ℂ} C)))$
136	133 135	mpbid	$⊢ φ \to (G : Y ⟶ ℂ \land G (C) \in (G {lim}_{ℂ} C))$
137	136	simprd	$⊢ φ \to G (C) \in (G {lim}_{ℂ} C)$
138		difss	$⊢ (X \cap Y) ∖ \{C\} \subseteq X \cap Y$
139	138 59	sstri	$⊢ (X \cap Y) ∖ \{C\} \subseteq Y$
140	139	a1i	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq Y$
141		eqid	$⊢ J ↾_{𝑡} (Y \cup \{C\}) = J ↾_{𝑡} (Y \cup \{C\})$
142		difssd	$⊢ φ \to ⋃ (J ↾_{𝑡} S) ∖ Y \subseteq ⋃ (J ↾_{𝑡} S)$
143	87 142	unssd	$⊢ φ \to (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y) \subseteq ⋃ (J ↾_{𝑡} S)$
144		ssun1	$⊢ X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)$
145	144	a1i	$⊢ φ \to X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)$
146	30	ntrss	$⊢ (J ↾_{𝑡} S \in Top \land (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y) \subseteq ⋃ (J ↾_{𝑡} S) \land X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y))$
147	25 143 145 146	syl3anc	$⊢ φ \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y))$
148	147 33	sseldd	$⊢ φ \to C \in int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y))$
149	148 71	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y)$
150	59	a1i	$⊢ φ \to X \cap Y \subseteq Y$
151		eqid	$⊢ (J ↾_{𝑡} S) ↾_{𝑡} Y = (J ↾_{𝑡} S) ↾_{𝑡} Y$
152	30 151	restntr	$⊢ (J ↾_{𝑡} S \in Top \land Y \subseteq ⋃ (J ↾_{𝑡} S) \land X \cap Y \subseteq Y) \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y$
153	25 29 150 152	syl3anc	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y$
154		restabs	$⊢ (J \in Top \land Y \subseteq S \land S \in V) \to (J ↾_{𝑡} S) ↾_{𝑡} Y = J ↾_{𝑡} Y$
155	101 4 104 154	syl3anc	$⊢ φ \to (J ↾_{𝑡} S) ↾_{𝑡} Y = J ↾_{𝑡} Y$
156	155	fveq2d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) = int (J ↾_{𝑡} Y)$
157	156	fveq1d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) (X \cap Y) = int (J ↾_{𝑡} Y) (X \cap Y)$
158	153 157	eqtr3d	$⊢ φ \to int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y = int (J ↾_{𝑡} Y) (X \cap Y)$
159	149 158	eleqtrd	$⊢ φ \to C \in int (J ↾_{𝑡} Y) (X \cap Y)$
160	71	snssd	$⊢ φ \to \{C\} \subseteq Y$
161		ssequn2	$⊢ \{C\} \subseteq Y \leftrightarrow Y \cup \{C\} = Y$
162	160 161	sylib	$⊢ φ \to Y \cup \{C\} = Y$
163	162	oveq2d	$⊢ φ \to J ↾_{𝑡} (Y \cup \{C\}) = J ↾_{𝑡} Y$
164	163	fveq2d	$⊢ φ \to int (J ↾_{𝑡} (Y \cup \{C\})) = int (J ↾_{𝑡} Y)$
165	164 123	fveq12d	$⊢ φ \to int (J ↾_{𝑡} (Y \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\}) = int (J ↾_{𝑡} Y) (X \cap Y)$
166	159 165	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} (Y \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\})$
167	3 140 66 10 141 166	limcres	$⊢ φ \to ({G ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = G {lim}_{ℂ} C$
168	3 140	feqresmpt	$⊢ φ \to {G ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ G (z))$
169	168	oveq1d	$⊢ φ \to ({G ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C$
170	167 169	eqtr3d	$⊢ φ \to G {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C$
171	137 170	eleqtrd	$⊢ φ \to G (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C)$
172	10	mulcn	$⊢ \times \in ((J \times_{t} J) Cn J)$
173	5 1 2	dvcl	$⊢ (φ \land C F_{S}^{'} K) \to K \in ℂ$
174	8 173	mpdan	$⊢ φ \to K \in ℂ$
175	3 71	ffvelrnd	$⊢ φ \to G (C) \in ℂ$
176	174 175	opelxpd	$⊢ φ \to ⟨K, G (C)⟩ \in (ℂ \times ℂ)$
177	77	toponunii	$⊢ ℂ \times ℂ = ⋃ (J \times_{t} J)$
178	177	cncnpi	$⊢ (\times \in ((J \times_{t} J) Cn J) \land ⟨K, G (C)⟩ \in (ℂ \times ℂ)) \to \times \in ((J \times_{t} J) CnP J) (⟨K, G (C)⟩)$
179	172 176 178	sylancr	$⊢ φ \to \times \in ((J \times_{t} J) CnP J) (⟨K, G (C)⟩)$
180	57 61 75 75 10 78 130 171 179	limccnp2	$⊢ φ \to K G (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z)) {lim}_{ℂ} C)$
181	18	simprd	$⊢ φ \to L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)$
182	72	fmpttd	$⊢ φ \to (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) : Y ∖ \{C\} ⟶ ℂ$
183	66	ssdifssd	$⊢ φ \to Y ∖ \{C\} \subseteq ℂ$
184		eqid	$⊢ J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})$
185		undif1	$⊢ (Y ∖ \{C\}) \cup \{C\} = Y \cup \{C\}$
186	185 162	syl5eq	$⊢ φ \to (Y ∖ \{C\}) \cup \{C\} = Y$
187	186	oveq2d	$⊢ φ \to J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} Y$
188	187	fveq2d	$⊢ φ \to int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) = int (J ↾_{𝑡} Y)$
189	188 123	fveq12d	$⊢ φ \to int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\}) = int (J ↾_{𝑡} Y) (X \cap Y)$
190	159 189	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\})$
191	182 64 183 10 184 190	limcres	$⊢ φ \to ({(z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C$
192	64	resmptd	$⊢ φ \to {(z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
193	192	oveq1d	$⊢ φ \to ({(z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C$
194	191 193	eqtr3d	$⊢ φ \to (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C$
195	181 194	eleqtrd	$⊢ φ \to L \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)$
196	86 5	sstrd	$⊢ φ \to X \cap Y \subseteq ℂ$
197		cncfmptc	$⊢ (F (C) \in ℂ \land X \cap Y \subseteq ℂ \land ℂ \subseteq ℂ) \to (z \in (X \cap Y) ⟼ F (C)) : (X \cap Y) \underset{cn}{⟶} ℂ$
198	45 196 75 197	syl3anc	$⊢ φ \to (z \in (X \cap Y) ⟼ F (C)) : (X \cap Y) \underset{cn}{⟶} ℂ$
199		eqidd	$⊢ z = C \to F (C) = F (C)$
200	198 119 199	cnmptlimc	$⊢ φ \to F (C) \in ((z \in (X \cap Y) ⟼ F (C)) {lim}_{ℂ} C)$
201	45	adantr	$⊢ (φ \land z \in (X \cap Y)) \to F (C) \in ℂ$
202	201	fmpttd	$⊢ φ \to (z \in (X \cap Y) ⟼ F (C)) : X \cap Y ⟶ ℂ$
203	202	limcdif	$⊢ φ \to (z \in (X \cap Y) ⟼ F (C)) {lim}_{ℂ} C = ({(z \in (X \cap Y) ⟼ F (C)) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C$
204		resmpt	$⊢ (X \cap Y) ∖ \{C\} \subseteq X \cap Y \to {(z \in (X \cap Y) ⟼ F (C)) ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C))$
205	138 204	mp1i	$⊢ φ \to {(z \in (X \cap Y) ⟼ F (C)) ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C))$
206	205	oveq1d	$⊢ φ \to ({(z \in (X \cap Y) ⟼ F (C)) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C)) {lim}_{ℂ} C$
207	203 206	eqtrd	$⊢ φ \to (z \in (X \cap Y) ⟼ F (C)) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C)) {lim}_{ℂ} C$
208	200 207	eleqtrd	$⊢ φ \to F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C)) {lim}_{ℂ} C)$
209	5 3 4	dvcl	$⊢ (φ \land C G_{S}^{'} L) \to L \in ℂ$
210	9 209	mpdan	$⊢ φ \to L \in ℂ$
211	210 45	opelxpd	$⊢ φ \to ⟨L, F (C)⟩ \in (ℂ \times ℂ)$
212	177	cncnpi	$⊢ (\times \in ((J \times_{t} J) Cn J) \land ⟨L, F (C)⟩ \in (ℂ \times ℂ)) \to \times \in ((J \times_{t} J) CnP J) (⟨L, F (C)⟩)$
213	172 211 212	sylancr	$⊢ φ \to \times \in ((J \times_{t} J) CnP J) (⟨L, F (C)⟩)$
214	73 46 75 75 10 78 195 208 213	limccnp2	$⊢ φ \to L F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{G (z) - G (C)}{z - C}) F (C)) {lim}_{ℂ} C)$
215	10	addcn	$⊢ + \in ((J \times_{t} J) Cn J)$
216	174 175	mulcld	$⊢ φ \to K G (C) \in ℂ$
217	210 45	mulcld	$⊢ φ \to L F (C) \in ℂ$
218	216 217	opelxpd	$⊢ φ \to ⟨K G (C), L F (C)⟩ \in (ℂ \times ℂ)$
219	177	cncnpi	$⊢ (+ \in ((J \times_{t} J) Cn J) \land ⟨K G (C), L F (C)⟩ \in (ℂ \times ℂ)) \to + \in ((J \times_{t} J) CnP J) (⟨K G (C), L F (C)⟩)$
220	215 218 219	sylancr	$⊢ φ \to + \in ((J \times_{t} J) CnP J) (⟨K G (C), L F (C)⟩)$
221	62 74 75 75 10 78 180 214 220	limccnp2	$⊢ φ \to K G (C) + L F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C)) {lim}_{ℂ} C)$
222	44	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in X$
223	34 222	ffvelrnd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) \in ℂ$
224	39 223	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) - F (C) \in ℂ$
225	224 61	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) - F (C)) G (z) \in ℂ$
226	71	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in Y$
227	58 226	ffvelrnd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (C) \in ℂ$
228	61 227	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (z) - G (C) \in ℂ$
229	228 223	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (G (z) - G (C)) F (C) \in ℂ$
230	49 222	sseldd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in ℂ$
231	50 230	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z - C \in ℂ$
232	225 229 231 56	divdird	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F (z) - F (C)) G (z) + (G (z) - G (C)) F (C)}{z - C} = (\frac{(F (z) - F (C)) G (z)}{z - C}) + (\frac{(G (z) - G (C)) F (C)}{z - C})$
233	39 61	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) G (z) \in ℂ$
234	223 61	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) G (z) \in ℂ$
235	223 227	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) G (C) \in ℂ$
236	233 234 235	npncand	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) G (z) - F (C) G (z)) + F (C) G (z) - F (C) G (C) = F (z) G (z) - F (C) G (C)$
237	39 223 61	subdird	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) - F (C)) G (z) = F (z) G (z) - F (C) G (z)$
238	228 223	mulcomd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (G (z) - G (C)) F (C) = F (C) (G (z) - G (C))$
239	223 61 227	subdid	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) (G (z) - G (C)) = F (C) G (z) - F (C) G (C)$
240	238 239	eqtrd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (G (z) - G (C)) F (C) = F (C) G (z) - F (C) G (C)$
241	237 240	oveq12d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) - F (C)) G (z) + (G (z) - G (C)) F (C) = (F (z) G (z) - F (C) G (z)) + F (C) G (z) - F (C) G (C)$
242	1	ffnd	$⊢ φ \to F Fn X$
243	242	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F Fn X$
244	3	ffnd	$⊢ φ \to G Fn Y$
245	244	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G Fn Y$
246		ssexg	$⊢ (X \subseteq ℂ \land ℂ \in V) \to X \in V$
247	48 102 246	sylancl	$⊢ φ \to X \in V$
248	247	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to X \in V$
249		ssexg	$⊢ (Y \subseteq ℂ \land ℂ \in V) \to Y \in V$
250	66 102 249	sylancl	$⊢ φ \to Y \in V$
251	250	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to Y \in V$
252		eqid	$⊢ X \cap Y = X \cap Y$
253		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in X) \to F (z) = F (z)$
254		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in Y) \to G (z) = G (z)$
255	243 245 248 251 252 253 254	ofval	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in (X \cap Y)) \to (F \times_{f} G) (z) = F (z) G (z)$
256	37 255	mpdan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F \times_{f} G) (z) = F (z) G (z)$
257		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in X) \to F (C) = F (C)$
258		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in Y) \to G (C) = G (C)$
259	243 245 248 251 252 257 258	ofval	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in (X \cap Y)) \to (F \times_{f} G) (C) = F (C) G (C)$
260	119 259	mpidan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F \times_{f} G) (C) = F (C) G (C)$
261	256 260	oveq12d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F \times_{f} G) (z) - (F \times_{f} G) (C) = F (z) G (z) - F (C) G (C)$
262	236 241 261	3eqtr4d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) - F (C)) G (z) + (G (z) - G (C)) F (C) = (F \times_{f} G) (z) - (F \times_{f} G) (C)$
263	262	oveq1d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F (z) - F (C)) G (z) + (G (z) - G (C)) F (C)}{z - C} = \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}$
264	224 61 231 56	div23d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F (z) - F (C)) G (z)}{z - C} = (\frac{F (z) - F (C)}{z - C}) G (z)$
265	228 223 231 56	div23d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(G (z) - G (C)) F (C)}{z - C} = (\frac{G (z) - G (C)}{z - C}) F (C)$
266	264 265	oveq12d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (\frac{(F (z) - F (C)) G (z)}{z - C}) + (\frac{(G (z) - G (C)) F (C)}{z - C}) = (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C)$
267	232 263 266	3eqtr3d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C} = (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C)$
268	267	mpteq2dva	$⊢ φ \to (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C))$
269	268	oveq1d	$⊢ φ \to (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C)) {lim}_{ℂ} C$
270	221 269	eleqtrrd	$⊢ φ \to K G (C) + L F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) {lim}_{ℂ} C)$
271		eqid	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C})$
272		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
273	272	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
274	273 1 3 247 250 252	off	$⊢ φ \to (F \times_{f} G) : X \cap Y ⟶ ℂ$
275	11 10 271 5 274 86	eldv	$⊢ φ \to (C {(F \times_{f} G)}_{S}^{'} (K G (C) + L F (C)) \leftrightarrow (C \in int (J ↾_{𝑡} S) (X \cap Y) \land K G (C) + L F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) {lim}_{ℂ} C)))$
276	33 270 275	mpbir2and	$⊢ φ \to C {(F \times_{f} G)}_{S}^{'} (K G (C) + L F (C))$

Metamath Proof Explorer

Theorem dvmulbr

Proof