dvmulbrOLD

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

Metamath Proof Explorer

Theorem dvmulbrOLD

Proof