dvmptfprodlem

	Ref	Expression
Hypotheses	dvmptfprodlem.xph	$⊢ Ⅎ x φ$
	dvmptfprodlem.iph	$⊢ Ⅎ i φ$
	dvmptfprodlem.jph	$⊢ Ⅎ j φ$
	dvmptfprodlem.if	$⊢ \underline{Ⅎ} i F$
	dvmptfprodlem.jg	$⊢ \underline{Ⅎ} j G$
	dvmptfprodlem.a	$⊢ (φ \land i \in I \land x \in X) \to A \in ℂ$
	dvmptfprodlem.d	$⊢ φ \to D \in Fin$
	dvmptfprodlem.e	$⊢ φ \to E \in V$
	dvmptfprodlem.db	$⊢ φ \to \neg E \in D$
	dvmptfprodlem.ss	$⊢ φ \to D \cup \{E\} \subseteq I$
	dvmptfprodlem.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvmptfprodlem.c	$⊢ ((φ \land x \in X) \land j \in D) \to C \in ℂ$
	dvmptfprodlem.dvp	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in D} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A)$
	dvmptfprodlem.14	$⊢ (φ \land x \in X) \to G \in ℂ$
	dvmptfprodlem.dvf	$⊢ φ \to \frac{d (x \in X⟼ F)}{d_{S} x} = (x \in X ⟼ G)$
	dvmptfprodlem.f	$⊢ i = E \to A = F$
	dvmptfprodlem.cg	$⊢ j = E \to C = G$
Assertion	dvmptfprodlem	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in D \cup \{E\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in D \cup \{E\}} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A)$

Proof

Step	Hyp	Ref	Expression
1		dvmptfprodlem.xph	$⊢ Ⅎ x φ$
2		dvmptfprodlem.iph	$⊢ Ⅎ i φ$
3		dvmptfprodlem.jph	$⊢ Ⅎ j φ$
4		dvmptfprodlem.if	$⊢ \underline{Ⅎ} i F$
5		dvmptfprodlem.jg	$⊢ \underline{Ⅎ} j G$
6		dvmptfprodlem.a	$⊢ (φ \land i \in I \land x \in X) \to A \in ℂ$
7		dvmptfprodlem.d	$⊢ φ \to D \in Fin$
8		dvmptfprodlem.e	$⊢ φ \to E \in V$
9		dvmptfprodlem.db	$⊢ φ \to \neg E \in D$
10		dvmptfprodlem.ss	$⊢ φ \to D \cup \{E\} \subseteq I$
11		dvmptfprodlem.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
12		dvmptfprodlem.c	$⊢ ((φ \land x \in X) \land j \in D) \to C \in ℂ$
13		dvmptfprodlem.dvp	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in D} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A)$
14		dvmptfprodlem.14	$⊢ (φ \land x \in X) \to G \in ℂ$
15		dvmptfprodlem.dvf	$⊢ φ \to \frac{d (x \in X⟼ F)}{d_{S} x} = (x \in X ⟼ G)$
16		dvmptfprodlem.f	$⊢ i = E \to A = F$
17		dvmptfprodlem.cg	$⊢ j = E \to C = G$
18		nfcv	$⊢ \underline{Ⅎ} i x$
19		nfcv	$⊢ \underline{Ⅎ} i X$
20	18 19	nfel	$⊢ Ⅎ i x \in X$
21	2 20	nfan	$⊢ Ⅎ i (φ \land x \in X)$
22	4	a1i	$⊢ (φ \land x \in X) \to \underline{Ⅎ} i F$
23		snfi	$⊢ \{E\} \in Fin$
24	23	a1i	$⊢ φ \to \{E\} \in Fin$
25		unfi	$⊢ (D \in Fin \land \{E\} \in Fin) \to D \cup \{E\} \in Fin$
26	7 24 25	syl2anc	$⊢ φ \to D \cup \{E\} \in Fin$
27	26	adantr	$⊢ (φ \land x \in X) \to D \cup \{E\} \in Fin$
28		simpll	$⊢ ((φ \land x \in X) \land i \in (D \cup \{E\})) \to φ$
29	10	sselda	$⊢ (φ \land i \in (D \cup \{E\})) \to i \in I$
30	29	adantlr	$⊢ ((φ \land x \in X) \land i \in (D \cup \{E\})) \to i \in I$
31		simplr	$⊢ ((φ \land x \in X) \land i \in (D \cup \{E\})) \to x \in X$
32	28 30 31 6	syl3anc	$⊢ ((φ \land x \in X) \land i \in (D \cup \{E\})) \to A \in ℂ$
33		snidg	$⊢ E \in V \to E \in \{E\}$
34	8 33	syl	$⊢ φ \to E \in \{E\}$
35		elun2	$⊢ E \in \{E\} \to E \in (D \cup \{E\})$
36	34 35	syl	$⊢ φ \to E \in (D \cup \{E\})$
37	36	adantr	$⊢ (φ \land x \in X) \to E \in (D \cup \{E\})$
38	16	adantl	$⊢ ((φ \land x \in X) \land i = E) \to A = F$
39	21 22 27 32 37 38	fprodsplit1f	$⊢ (φ \land x \in X) \to \prod_{i \in D \cup \{E\}} A = F \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A$
40		difundir	$⊢ (D \cup \{E\}) ∖ \{E\} = (D ∖ \{E\}) \cup (\{E\} ∖ \{E\})$
41	40	a1i	$⊢ φ \to (D \cup \{E\}) ∖ \{E\} = (D ∖ \{E\}) \cup (\{E\} ∖ \{E\})$
42		difsn	$⊢ \neg E \in D \to D ∖ \{E\} = D$
43	9 42	syl	$⊢ φ \to D ∖ \{E\} = D$
44		difid	$⊢ \{E\} ∖ \{E\} = \emptyset$
45	44	a1i	$⊢ φ \to \{E\} ∖ \{E\} = \emptyset$
46	43 45	uneq12d	$⊢ φ \to (D ∖ \{E\}) \cup (\{E\} ∖ \{E\}) = D \cup \emptyset$
47		un0	$⊢ D \cup \emptyset = D$
48	47	a1i	$⊢ φ \to D \cup \emptyset = D$
49	41 46 48	3eqtrd	$⊢ φ \to (D \cup \{E\}) ∖ \{E\} = D$
50	49	prodeq1d	$⊢ φ \to \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A = \prod_{i \in D} A$
51	50	oveq2d	$⊢ φ \to F \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A = F \prod_{i \in D} A$
52	51	adantr	$⊢ (φ \land x \in X) \to F \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A = F \prod_{i \in D} A$
53	39 52	eqtrd	$⊢ (φ \land x \in X) \to \prod_{i \in D \cup \{E\}} A = F \prod_{i \in D} A$
54	1 53	mpteq2da	$⊢ φ \to (x \in X ⟼ \prod_{i \in D \cup \{E\}} A) = (x \in X ⟼ F \prod_{i \in D} A)$
55	54	oveq2d	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in D \cup \{E\}} A)}{d_{S} x} = \frac{d (x \in X⟼ F \prod_{i \in D} A)}{d_{S} x}$
56	10 36	sseldd	$⊢ φ \to E \in I$
57	56	adantr	$⊢ (φ \land x \in X) \to E \in I$
58		simpl	$⊢ (φ \land x \in X) \to φ$
59		simpr	$⊢ (φ \land x \in X) \to x \in X$
60	58 57 59	3jca	$⊢ (φ \land x \in X) \to (φ \land E \in I \land x \in X)$
61		nfcv	$⊢ \underline{Ⅎ} i E$
62		nfv	$⊢ Ⅎ i E \in I$
63	2 62 20	nf3an	$⊢ Ⅎ i (φ \land E \in I \land x \in X)$
64		nfcv	$⊢ \underline{Ⅎ} i ℂ$
65	4 64	nfel	$⊢ Ⅎ i F \in ℂ$
66	63 65	nfim	$⊢ Ⅎ i ((φ \land E \in I \land x \in X) \to F \in ℂ)$
67		ancom	$⊢ ((φ \land x \in X) \land i = E) \leftrightarrow (i = E \land (φ \land x \in X))$
68	67	imbi1i	$⊢ (((φ \land x \in X) \land i = E) \to A = F) \leftrightarrow ((i = E \land (φ \land x \in X)) \to A = F)$
69		eqcom	$⊢ A = F \leftrightarrow F = A$
70	69	imbi2i	$⊢ ((i = E \land (φ \land x \in X)) \to A = F) \leftrightarrow ((i = E \land (φ \land x \in X)) \to F = A)$
71	68 70	bitri	$⊢ (((φ \land x \in X) \land i = E) \to A = F) \leftrightarrow ((i = E \land (φ \land x \in X)) \to F = A)$
72	38 71	mpbi	$⊢ (i = E \land (φ \land x \in X)) \to F = A$
73	72	3adantr2	$⊢ (i = E \land (φ \land E \in I \land x \in X)) \to F = A$
74	73	3adant2	$⊢ (i = E \land ((φ \land i \in I \land x \in X) \to A \in ℂ) \land (φ \land E \in I \land x \in X)) \to F = A$
75		simp3	$⊢ (i = E \land ((φ \land i \in I \land x \in X) \to A \in ℂ) \land (φ \land E \in I \land x \in X)) \to (φ \land E \in I \land x \in X)$
76		eleq1	$⊢ i = E \to (i \in I \leftrightarrow E \in I)$
77	76	3anbi2d	$⊢ i = E \to ((φ \land i \in I \land x \in X) \leftrightarrow (φ \land E \in I \land x \in X))$
78	77	imbi1d	$⊢ i = E \to (((φ \land i \in I \land x \in X) \to A \in ℂ) \leftrightarrow ((φ \land E \in I \land x \in X) \to A \in ℂ))$
79	78	biimpa	$⊢ (i = E \land ((φ \land i \in I \land x \in X) \to A \in ℂ)) \to ((φ \land E \in I \land x \in X) \to A \in ℂ)$
80	79	3adant3	$⊢ (i = E \land ((φ \land i \in I \land x \in X) \to A \in ℂ) \land (φ \land E \in I \land x \in X)) \to ((φ \land E \in I \land x \in X) \to A \in ℂ)$
81	75 80	mpd	$⊢ (i = E \land ((φ \land i \in I \land x \in X) \to A \in ℂ) \land (φ \land E \in I \land x \in X)) \to A \in ℂ$
82	74 81	eqeltrd	$⊢ (i = E \land ((φ \land i \in I \land x \in X) \to A \in ℂ) \land (φ \land E \in I \land x \in X)) \to F \in ℂ$
83	82	3exp	$⊢ i = E \to (((φ \land i \in I \land x \in X) \to A \in ℂ) \to ((φ \land E \in I \land x \in X) \to F \in ℂ))$
84	6	2a1i	$⊢ i = E \to (((φ \land E \in I \land x \in X) \to F \in ℂ) \to ((φ \land i \in I \land x \in X) \to A \in ℂ))$
85	83 84	impbid	$⊢ i = E \to (((φ \land i \in I \land x \in X) \to A \in ℂ) \leftrightarrow ((φ \land E \in I \land x \in X) \to F \in ℂ))$
86	61 66 85 6	vtoclgf	$⊢ E \in I \to ((φ \land E \in I \land x \in X) \to F \in ℂ)$
87	57 60 86	sylc	$⊢ (φ \land x \in X) \to F \in ℂ$
88	58 7	syl	$⊢ (φ \land x \in X) \to D \in Fin$
89	58	adantr	$⊢ ((φ \land x \in X) \land i \in D) \to φ$
90	10	adantr	$⊢ (φ \land i \in D) \to D \cup \{E\} \subseteq I$
91		elun1	$⊢ i \in D \to i \in (D \cup \{E\})$
92	91	adantl	$⊢ (φ \land i \in D) \to i \in (D \cup \{E\})$
93	90 92	sseldd	$⊢ (φ \land i \in D) \to i \in I$
94	93	adantlr	$⊢ ((φ \land x \in X) \land i \in D) \to i \in I$
95	59	adantr	$⊢ ((φ \land x \in X) \land i \in D) \to x \in X$
96	89 94 95 6	syl3anc	$⊢ ((φ \land x \in X) \land i \in D) \to A \in ℂ$
97	21 88 96	fprodclf	$⊢ (φ \land x \in X) \to \prod_{i \in D} A \in ℂ$
98		nfv	$⊢ Ⅎ j x \in X$
99	3 98	nfan	$⊢ Ⅎ j (φ \land x \in X)$
100		diffi	$⊢ D \in Fin \to D ∖ \{j\} \in Fin$
101	7 100	syl	$⊢ φ \to D ∖ \{j\} \in Fin$
102	101	adantr	$⊢ (φ \land x \in X) \to D ∖ \{j\} \in Fin$
103		eldifi	$⊢ i \in (D ∖ \{j\}) \to i \in D$
104	103	adantl	$⊢ ((φ \land x \in X) \land i \in (D ∖ \{j\})) \to i \in D$
105	104 96	syldan	$⊢ ((φ \land x \in X) \land i \in (D ∖ \{j\})) \to A \in ℂ$
106	21 102 105	fprodclf	$⊢ (φ \land x \in X) \to \prod_{i \in D ∖ \{j\}} A \in ℂ$
107	106	adantr	$⊢ ((φ \land x \in X) \land j \in D) \to \prod_{i \in D ∖ \{j\}} A \in ℂ$
108	12 107	mulcld	$⊢ ((φ \land x \in X) \land j \in D) \to C \prod_{i \in D ∖ \{j\}} A \in ℂ$
109	99 88 108	fsumclf	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A \in ℂ$
110	1 11 87 14 15 97 109 13	dvmptmulf	$⊢ φ \to \frac{d (x \in X⟼ F \prod_{i \in D} A)}{d_{S} x} = (x \in X ⟼ G \prod_{i \in D} A + \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F)$
111		nfcv	$⊢ \underline{Ⅎ} j \times$
112		nfcv	$⊢ \underline{Ⅎ} j \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A$
113	5 111 112	nfov	$⊢ \underline{Ⅎ} j G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A$
114	58 8	syl	$⊢ (φ \land x \in X) \to E \in V$
115	58 9	syl	$⊢ (φ \land x \in X) \to \neg E \in D$
116		diffi	$⊢ D \cup \{E\} \in Fin \to (D \cup \{E\}) ∖ \{j\} \in Fin$
117	26 116	syl	$⊢ φ \to (D \cup \{E\}) ∖ \{j\} \in Fin$
118	117	adantr	$⊢ (φ \land x \in X) \to (D \cup \{E\}) ∖ \{j\} \in Fin$
119		eldifi	$⊢ i \in ((D \cup \{E\}) ∖ \{j\}) \to i \in (D \cup \{E\})$
120	119	adantl	$⊢ ((φ \land x \in X) \land i \in ((D \cup \{E\}) ∖ \{j\})) \to i \in (D \cup \{E\})$
121	120 32	syldan	$⊢ ((φ \land x \in X) \land i \in ((D \cup \{E\}) ∖ \{j\})) \to A \in ℂ$
122	21 118 121	fprodclf	$⊢ (φ \land x \in X) \to \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A \in ℂ$
123	122	adantr	$⊢ ((φ \land x \in X) \land j \in D) \to \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A \in ℂ$
124	12 123	mulcld	$⊢ ((φ \land x \in X) \land j \in D) \to C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A \in ℂ$
125		sneq	$⊢ j = E \to \{j\} = \{E\}$
126	125	difeq2d	$⊢ j = E \to (D \cup \{E\}) ∖ \{j\} = (D \cup \{E\}) ∖ \{E\}$
127	126	prodeq1d	$⊢ j = E \to \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A$
128	17 127	oveq12d	$⊢ j = E \to C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A$
129	49 7	eqeltrd	$⊢ φ \to (D \cup \{E\}) ∖ \{E\} \in Fin$
130	129	adantr	$⊢ (φ \land x \in X) \to (D \cup \{E\}) ∖ \{E\} \in Fin$
131	58	adantr	$⊢ ((φ \land x \in X) \land i \in ((D \cup \{E\}) ∖ \{E\})) \to φ$
132	10	adantr	$⊢ (φ \land i \in ((D \cup \{E\}) ∖ \{E\})) \to D \cup \{E\} \subseteq I$
133		eldifi	$⊢ i \in ((D \cup \{E\}) ∖ \{E\}) \to i \in (D \cup \{E\})$
134	133	adantl	$⊢ (φ \land i \in ((D \cup \{E\}) ∖ \{E\})) \to i \in (D \cup \{E\})$
135	132 134	sseldd	$⊢ (φ \land i \in ((D \cup \{E\}) ∖ \{E\})) \to i \in I$
136	135	adantlr	$⊢ ((φ \land x \in X) \land i \in ((D \cup \{E\}) ∖ \{E\})) \to i \in I$
137	59	adantr	$⊢ ((φ \land x \in X) \land i \in ((D \cup \{E\}) ∖ \{E\})) \to x \in X$
138	131 136 137 6	syl3anc	$⊢ ((φ \land x \in X) \land i \in ((D \cup \{E\}) ∖ \{E\})) \to A \in ℂ$
139	21 130 138	fprodclf	$⊢ (φ \land x \in X) \to \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A \in ℂ$
140	14 139	mulcld	$⊢ (φ \land x \in X) \to G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A \in ℂ$
141	99 113 88 114 115 124 128 140	fsumsplitsn	$⊢ (φ \land x \in X) \to \sum_{j \in D \cup \{E\}} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = \sum_{j \in D} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A + G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A$
142		difundir	$⊢ (D \cup \{E\}) ∖ \{j\} = (D ∖ \{j\}) \cup (\{E\} ∖ \{j\})$
143	142	a1i	$⊢ (φ \land j \in D) \to (D \cup \{E\}) ∖ \{j\} = (D ∖ \{j\}) \cup (\{E\} ∖ \{j\})$
144		nfv	$⊢ Ⅎ x j \in D$
145	1 144	nfan	$⊢ Ⅎ x (φ \land j \in D)$
146		elsni	$⊢ x \in \{E\} \to x = E$
147	146	eqcomd	$⊢ x \in \{E\} \to E = x$
148	147	adantr	$⊢ (x \in \{E\} \land x = j) \to E = x$
149		simpr	$⊢ (x \in \{E\} \land x = j) \to x = j$
150		eqidd	$⊢ (x \in \{E\} \land x = j) \to j = j$
151	148 149 150	3eqtrd	$⊢ (x \in \{E\} \land x = j) \to E = j$
152	151	adantll	$⊢ (((φ \land j \in D) \land x \in \{E\}) \land x = j) \to E = j$
153		simpllr	$⊢ (((φ \land j \in D) \land x \in \{E\}) \land x = j) \to j \in D$
154	152 153	eqeltrd	$⊢ (((φ \land j \in D) \land x \in \{E\}) \land x = j) \to E \in D$
155	9	ad3antrrr	$⊢ (((φ \land j \in D) \land x \in \{E\}) \land x = j) \to \neg E \in D$
156	154 155	pm2.65da	$⊢ ((φ \land j \in D) \land x \in \{E\}) \to \neg x = j$
157		velsn	$⊢ x \in \{j\} \leftrightarrow x = j$
158	156 157	sylnibr	$⊢ ((φ \land j \in D) \land x \in \{E\}) \to \neg x \in \{j\}$
159	158	ex	$⊢ (φ \land j \in D) \to (x \in \{E\} \to \neg x \in \{j\})$
160	145 159	ralrimi	$⊢ (φ \land j \in D) \to \forall x \in \{E\} \neg x \in \{j\}$
161		disj	$⊢ \{E\} \cap \{j\} = \emptyset \leftrightarrow \forall x \in \{E\} \neg x \in \{j\}$
162	160 161	sylibr	$⊢ (φ \land j \in D) \to \{E\} \cap \{j\} = \emptyset$
163		disjdif2	$⊢ \{E\} \cap \{j\} = \emptyset \to \{E\} ∖ \{j\} = \{E\}$
164	162 163	syl	$⊢ (φ \land j \in D) \to \{E\} ∖ \{j\} = \{E\}$
165	164	uneq2d	$⊢ (φ \land j \in D) \to (D ∖ \{j\}) \cup (\{E\} ∖ \{j\}) = (D ∖ \{j\}) \cup \{E\}$
166	143 165	eqtrd	$⊢ (φ \land j \in D) \to (D \cup \{E\}) ∖ \{j\} = (D ∖ \{j\}) \cup \{E\}$
167	166	prodeq1d	$⊢ (φ \land j \in D) \to \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = \prod_{i \in (D ∖ \{j\}) \cup \{E\}} A$
168	167	adantlr	$⊢ ((φ \land x \in X) \land j \in D) \to \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = \prod_{i \in (D ∖ \{j\}) \cup \{E\}} A$
169		nfv	$⊢ Ⅎ i j \in D$
170	21 169	nfan	$⊢ Ⅎ i ((φ \land x \in X) \land j \in D)$
171	102	adantr	$⊢ ((φ \land x \in X) \land j \in D) \to D ∖ \{j\} \in Fin$
172	58	adantr	$⊢ ((φ \land x \in X) \land j \in D) \to φ$
173	172 8	syl	$⊢ ((φ \land x \in X) \land j \in D) \to E \in V$
174		id	$⊢ \neg E \in D \to \neg E \in D$
175	174	intnanrd	$⊢ \neg E \in D \to \neg (E \in D \land \neg E \in \{j\})$
176	174 175	syl	$⊢ \neg E \in D \to \neg (E \in D \land \neg E \in \{j\})$
177		eldif	$⊢ E \in (D ∖ \{j\}) \leftrightarrow (E \in D \land \neg E \in \{j\})$
178	176 177	sylnibr	$⊢ \neg E \in D \to \neg E \in (D ∖ \{j\})$
179	9 178	syl	$⊢ φ \to \neg E \in (D ∖ \{j\})$
180	172 179	syl	$⊢ ((φ \land x \in X) \land j \in D) \to \neg E \in (D ∖ \{j\})$
181	105	adantlr	$⊢ (((φ \land x \in X) \land j \in D) \land i \in (D ∖ \{j\})) \to A \in ℂ$
182	87	adantr	$⊢ ((φ \land x \in X) \land j \in D) \to F \in ℂ$
183	170 4 171 173 180 181 16 182	fprodsplitsn	$⊢ ((φ \land x \in X) \land j \in D) \to \prod_{i \in (D ∖ \{j\}) \cup \{E\}} A = \prod_{i \in D ∖ \{j\}} A F$
184		eqidd	$⊢ ((φ \land x \in X) \land j \in D) \to \prod_{i \in D ∖ \{j\}} A F = \prod_{i \in D ∖ \{j\}} A F$
185	168 183 184	3eqtrd	$⊢ ((φ \land x \in X) \land j \in D) \to \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = \prod_{i \in D ∖ \{j\}} A F$
186	185	oveq2d	$⊢ ((φ \land x \in X) \land j \in D) \to C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = C \prod_{i \in D ∖ \{j\}} A F$
187	12 107 182	mulassd	$⊢ ((φ \land x \in X) \land j \in D) \to C \prod_{i \in D ∖ \{j\}} A F = C \prod_{i \in D ∖ \{j\}} A F$
188	187	eqcomd	$⊢ ((φ \land x \in X) \land j \in D) \to C \prod_{i \in D ∖ \{j\}} A F = C \prod_{i \in D ∖ \{j\}} A F$
189	186 188	eqtrd	$⊢ ((φ \land x \in X) \land j \in D) \to C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = C \prod_{i \in D ∖ \{j\}} A F$
190	189	ex	$⊢ (φ \land x \in X) \to (j \in D \to C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = C \prod_{i \in D ∖ \{j\}} A F)$
191	99 190	ralrimi	$⊢ (φ \land x \in X) \to \forall j \in D C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = C \prod_{i \in D ∖ \{j\}} A F$
192	191	sumeq2d	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F$
193	99 88 87 108	fsummulc1f	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F = \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F$
194	193	eqcomd	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F = \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F$
195		eqidd	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F = \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F$
196	192 194 195	3eqtrd	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F$
197	109 87	mulcld	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F \in ℂ$
198	196 197	eqeltrd	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A \in ℂ$
199	198 140	addcomd	$⊢ (φ \land x \in X) \to \sum_{j \in D} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A + G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A = G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A + \sum_{j \in D} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A$
200	50	oveq2d	$⊢ φ \to G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A = G \prod_{i \in D} A$
201	200	adantr	$⊢ (φ \land x \in X) \to G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A = G \prod_{i \in D} A$
202	201 196	oveq12d	$⊢ (φ \land x \in X) \to G \prod_{i \in (D \cup \{E\}) ∖ \{E\}} A + \sum_{j \in D} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A = G \prod_{i \in D} A + \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F$
203	141 199 202	3eqtrrd	$⊢ (φ \land x \in X) \to G \prod_{i \in D} A + \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F = \sum_{j \in D \cup \{E\}} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A$
204	1 203	mpteq2da	$⊢ φ \to (x \in X ⟼ G \prod_{i \in D} A + \sum_{j \in D} C \prod_{i \in D ∖ \{j\}} A F) = (x \in X ⟼ \sum_{j \in D \cup \{E\}} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A)$
205	55 110 204	3eqtrd	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in D \cup \{E\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in D \cup \{E\}} C \prod_{i \in (D \cup \{E\}) ∖ \{j\}} A)$

Metamath Proof Explorer

Theorem dvmptfprodlem

Proof