dvmptfprod

Description: Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvmptfprod.iph	$⊢ Ⅎ i φ$
	dvmptfprod.jph	$⊢ Ⅎ j φ$
	dvmptfprod.j	$⊢ J = K ↾_{𝑡} S$
	dvmptfprod.k	$⊢ K = TopOpen (ℂ_{fld})$
	dvmptfprod.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvmptfprod.x	$⊢ φ \to X \in J$
	dvmptfprod.i	$⊢ φ \to I \in Fin$
	dvmptfprod.a	$⊢ (φ \land i \in I \land x \in X) \to A \in ℂ$
	dvmptfprod.b	$⊢ (φ \land i \in I \land x \in X) \to B \in ℂ$
	dvmptfprod.d	$⊢ (φ \land i \in I) \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B)$
	dvmptfprod.bc	$⊢ i = j \to B = C$
Assertion	dvmptfprod	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in I} C \prod_{i \in I ∖ \{j\}} A)$

Proof

Step	Hyp	Ref	Expression
1		dvmptfprod.iph	$⊢ Ⅎ i φ$
2		dvmptfprod.jph	$⊢ Ⅎ j φ$
3		dvmptfprod.j	$⊢ J = K ↾_{𝑡} S$
4		dvmptfprod.k	$⊢ K = TopOpen (ℂ_{fld})$
5		dvmptfprod.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
6		dvmptfprod.x	$⊢ φ \to X \in J$
7		dvmptfprod.i	$⊢ φ \to I \in Fin$
8		dvmptfprod.a	$⊢ (φ \land i \in I \land x \in X) \to A \in ℂ$
9		dvmptfprod.b	$⊢ (φ \land i \in I \land x \in X) \to B \in ℂ$
10		dvmptfprod.d	$⊢ (φ \land i \in I) \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B)$
11		dvmptfprod.bc	$⊢ i = j \to B = C$
12		ssid	$⊢ I \subseteq I$
13	12	jctr	$⊢ φ \to (φ \land I \subseteq I)$
14		sseq1	$⊢ a = \emptyset \to (a \subseteq I \leftrightarrow \emptyset \subseteq I)$
15	14	anbi2d	$⊢ a = \emptyset \to ((φ \land a \subseteq I) \leftrightarrow (φ \land \emptyset \subseteq I))$
16		prodeq1	$⊢ a = \emptyset \to \prod_{i \in a} A = \prod_{i \in \emptyset} A$
17	16	mpteq2dv	$⊢ a = \emptyset \to (x \in X ⟼ \prod_{i \in a} A) = (x \in X ⟼ \prod_{i \in \emptyset} A)$
18	17	oveq2d	$⊢ a = \emptyset \to \frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x}$
19		sumeq1	$⊢ a = \emptyset \to \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in \emptyset} C \prod_{i \in a ∖ \{j\}} A$
20		difeq1	$⊢ a = \emptyset \to a ∖ \{j\} = \emptyset ∖ \{j\}$
21	20	prodeq1d	$⊢ a = \emptyset \to \prod_{i \in a ∖ \{j\}} A = \prod_{i \in \emptyset ∖ \{j\}} A$
22	21	oveq2d	$⊢ a = \emptyset \to C \prod_{i \in a ∖ \{j\}} A = C \prod_{i \in \emptyset ∖ \{j\}} A$
23	22	sumeq2sdv	$⊢ a = \emptyset \to \sum_{j \in \emptyset} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A$
24	19 23	eqtrd	$⊢ a = \emptyset \to \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A$
25	24	mpteq2dv	$⊢ a = \emptyset \to (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A) = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A)$
26	18 25	eqeq12d	$⊢ a = \emptyset \to (\frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A) \leftrightarrow \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A))$
27	15 26	imbi12d	$⊢ a = \emptyset \to (((φ \land a \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A)) \leftrightarrow ((φ \land \emptyset \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A)))$
28		sseq1	$⊢ a = b \to (a \subseteq I \leftrightarrow b \subseteq I)$
29	28	anbi2d	$⊢ a = b \to ((φ \land a \subseteq I) \leftrightarrow (φ \land b \subseteq I))$
30		prodeq1	$⊢ a = b \to \prod_{i \in a} A = \prod_{i \in b} A$
31	30	mpteq2dv	$⊢ a = b \to (x \in X ⟼ \prod_{i \in a} A) = (x \in X ⟼ \prod_{i \in b} A)$
32	31	oveq2d	$⊢ a = b \to \frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x}$
33		sumeq1	$⊢ a = b \to \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in b} C \prod_{i \in a ∖ \{j\}} A$
34		difeq1	$⊢ a = b \to a ∖ \{j\} = b ∖ \{j\}$
35	34	prodeq1d	$⊢ a = b \to \prod_{i \in a ∖ \{j\}} A = \prod_{i \in b ∖ \{j\}} A$
36	35	oveq2d	$⊢ a = b \to C \prod_{i \in a ∖ \{j\}} A = C \prod_{i \in b ∖ \{j\}} A$
37	36	sumeq2sdv	$⊢ a = b \to \sum_{j \in b} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A$
38	33 37	eqtrd	$⊢ a = b \to \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A$
39	38	mpteq2dv	$⊢ a = b \to (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A) = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
40	32 39	eqeq12d	$⊢ a = b \to (\frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A) \leftrightarrow \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A))$
41	29 40	imbi12d	$⊢ a = b \to (((φ \land a \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A)) \leftrightarrow ((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)))$
42		sseq1	$⊢ a = b \cup \{c\} \to (a \subseteq I \leftrightarrow b \cup \{c\} \subseteq I)$
43	42	anbi2d	$⊢ a = b \cup \{c\} \to ((φ \land a \subseteq I) \leftrightarrow (φ \land b \cup \{c\} \subseteq I))$
44		prodeq1	$⊢ a = b \cup \{c\} \to \prod_{i \in a} A = \prod_{i \in b \cup \{c\}} A$
45	44	mpteq2dv	$⊢ a = b \cup \{c\} \to (x \in X ⟼ \prod_{i \in a} A) = (x \in X ⟼ \prod_{i \in b \cup \{c\}} A)$
46	45	oveq2d	$⊢ a = b \cup \{c\} \to \frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = \frac{d (x \in X⟼ \prod_{i \in b \cup \{c\}} A)}{d_{S} x}$
47		sumeq1	$⊢ a = b \cup \{c\} \to \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in b \cup \{c\}} C \prod_{i \in a ∖ \{j\}} A$
48		difeq1	$⊢ a = b \cup \{c\} \to a ∖ \{j\} = (b \cup \{c\}) ∖ \{j\}$
49	48	prodeq1d	$⊢ a = b \cup \{c\} \to \prod_{i \in a ∖ \{j\}} A = \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A$
50	49	oveq2d	$⊢ a = b \cup \{c\} \to C \prod_{i \in a ∖ \{j\}} A = C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A$
51	50	sumeq2sdv	$⊢ a = b \cup \{c\} \to \sum_{j \in b \cup \{c\}} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in b \cup \{c\}} C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A$
52	47 51	eqtrd	$⊢ a = b \cup \{c\} \to \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in b \cup \{c\}} C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A$
53	52	mpteq2dv	$⊢ a = b \cup \{c\} \to (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A) = (x \in X ⟼ \sum_{j \in b \cup \{c\}} C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A)$
54	46 53	eqeq12d	$⊢ a = b \cup \{c\} \to (\frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A) \leftrightarrow \frac{d (x \in X⟼ \prod_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b \cup \{c\}} C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A))$
55	43 54	imbi12d	$⊢ a = b \cup \{c\} \to (((φ \land a \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A)) \leftrightarrow ((φ \land b \cup \{c\} \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b \cup \{c\}} C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A)))$
56		sseq1	$⊢ a = I \to (a \subseteq I \leftrightarrow I \subseteq I)$
57	56	anbi2d	$⊢ a = I \to ((φ \land a \subseteq I) \leftrightarrow (φ \land I \subseteq I))$
58		prodeq1	$⊢ a = I \to \prod_{i \in a} A = \prod_{i \in I} A$
59	58	mpteq2dv	$⊢ a = I \to (x \in X ⟼ \prod_{i \in a} A) = (x \in X ⟼ \prod_{i \in I} A)$
60	59	oveq2d	$⊢ a = I \to \frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = \frac{d (x \in X⟼ \prod_{i \in I} A)}{d_{S} x}$
61		sumeq1	$⊢ a = I \to \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in I} C \prod_{i \in a ∖ \{j\}} A$
62		difeq1	$⊢ a = I \to a ∖ \{j\} = I ∖ \{j\}$
63	62	prodeq1d	$⊢ a = I \to \prod_{i \in a ∖ \{j\}} A = \prod_{i \in I ∖ \{j\}} A$
64	63	oveq2d	$⊢ a = I \to C \prod_{i \in a ∖ \{j\}} A = C \prod_{i \in I ∖ \{j\}} A$
65	64	sumeq2sdv	$⊢ a = I \to \sum_{j \in I} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in I} C \prod_{i \in I ∖ \{j\}} A$
66	61 65	eqtrd	$⊢ a = I \to \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A = \sum_{j \in I} C \prod_{i \in I ∖ \{j\}} A$
67	66	mpteq2dv	$⊢ a = I \to (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A) = (x \in X ⟼ \sum_{j \in I} C \prod_{i \in I ∖ \{j\}} A)$
68	60 67	eqeq12d	$⊢ a = I \to (\frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A) \leftrightarrow \frac{d (x \in X⟼ \prod_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in I} C \prod_{i \in I ∖ \{j\}} A))$
69	57 68	imbi12d	$⊢ a = I \to (((φ \land a \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in a} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in a} C \prod_{i \in a ∖ \{j\}} A)) \leftrightarrow ((φ \land I \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in I} C \prod_{i \in I ∖ \{j\}} A)))$
70		prod0	$⊢ \prod_{i \in \emptyset} A = 1$
71	70	mpteq2i	$⊢ (x \in X ⟼ \prod_{i \in \emptyset} A) = (x \in X ⟼ 1)$
72	71	oveq2i	$⊢ \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x} = \frac{d (x \in X⟼ 1)}{d_{S} x}$
73	72	a1i	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x} = \frac{d (x \in X⟼ 1)}{d_{S} x}$
74	4	oveq1i	$⊢ K ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
75	3 74	eqtri	$⊢ J = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
76	6 75	eleqtrdi	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
77		1cnd	$⊢ φ \to 1 \in ℂ$
78	5 76 77	dvmptconst	$⊢ φ \to \frac{d (x \in X⟼ 1)}{d_{S} x} = (x \in X ⟼ 0)$
79		sum0	$⊢ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A = 0$
80	79	eqcomi	$⊢ 0 = \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A$
81	80	mpteq2i	$⊢ (x \in X ⟼ 0) = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A)$
82	81	a1i	$⊢ φ \to (x \in X ⟼ 0) = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A)$
83	73 78 82	3eqtrd	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A)$
84	83	adantr	$⊢ (φ \land \emptyset \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A)$
85		simp3	$⊢ ((b \in Fin \land \neg c \in b) \land ((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land (φ \land b \cup \{c\} \subseteq I)) \to (φ \land b \cup \{c\} \subseteq I)$
86		simp1r	$⊢ ((b \in Fin \land \neg c \in b) \land ((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land (φ \land b \cup \{c\} \subseteq I)) \to \neg c \in b$
87		ssun1	$⊢ b \subseteq b \cup \{c\}$
88		sstr2	$⊢ b \subseteq b \cup \{c\} \to (b \cup \{c\} \subseteq I \to b \subseteq I)$
89	87 88	ax-mp	$⊢ b \cup \{c\} \subseteq I \to b \subseteq I$
90	89	anim2i	$⊢ (φ \land b \cup \{c\} \subseteq I) \to (φ \land b \subseteq I)$
91	90	adantl	$⊢ (((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land (φ \land b \cup \{c\} \subseteq I)) \to (φ \land b \subseteq I)$
92		simpl	$⊢ (((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land (φ \land b \cup \{c\} \subseteq I)) \to ((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A))$
93	91 92	mpd	$⊢ (((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land (φ \land b \cup \{c\} \subseteq I)) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
94	93	3adant1	$⊢ ((b \in Fin \land \neg c \in b) \land ((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land (φ \land b \cup \{c\} \subseteq I)) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
95		nfv	$⊢ Ⅎ x ((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b)$
96		nfcv	$⊢ \underline{Ⅎ} x S$
97		nfcv	$⊢ \underline{Ⅎ} x D$
98		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ \prod_{i \in b} A)$
99	96 97 98	nfov	$⊢ \underline{Ⅎ} x \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x}$
100		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
101	99 100	nfeq	$⊢ Ⅎ x \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
102	95 101	nfan	$⊢ Ⅎ x (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A))$
103		nfv	$⊢ Ⅎ i b \cup \{c\} \subseteq I$
104	1 103	nfan	$⊢ Ⅎ i (φ \land b \cup \{c\} \subseteq I)$
105		nfv	$⊢ Ⅎ i \neg c \in b$
106	104 105	nfan	$⊢ Ⅎ i ((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b)$
107		nfcv	$⊢ \underline{Ⅎ} i S$
108		nfcv	$⊢ \underline{Ⅎ} i D$
109		nfcv	$⊢ \underline{Ⅎ} i X$
110		nfcv	$⊢ \underline{Ⅎ} i b$
111	110	nfcprod1	$⊢ \underline{Ⅎ} i \prod_{i \in b} A$
112	109 111	nfmpt	$⊢ \underline{Ⅎ} i (x \in X ⟼ \prod_{i \in b} A)$
113	107 108 112	nfov	$⊢ \underline{Ⅎ} i \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x}$
114		nfcv	$⊢ \underline{Ⅎ} i C$
115		nfcv	$⊢ \underline{Ⅎ} i \times$
116		nfcv	$⊢ \underline{Ⅎ} i (b ∖ \{j\})$
117	116	nfcprod1	$⊢ \underline{Ⅎ} i \prod_{i \in b ∖ \{j\}} A$
118	114 115 117	nfov	$⊢ \underline{Ⅎ} i C \prod_{i \in b ∖ \{j\}} A$
119	110 118	nfsum	$⊢ \underline{Ⅎ} i \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A$
120	109 119	nfmpt	$⊢ \underline{Ⅎ} i (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
121	113 120	nfeq	$⊢ Ⅎ i \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
122	106 121	nfan	$⊢ Ⅎ i (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A))$
123		nfv	$⊢ Ⅎ j b \cup \{c\} \subseteq I$
124	2 123	nfan	$⊢ Ⅎ j (φ \land b \cup \{c\} \subseteq I)$
125		nfv	$⊢ Ⅎ j \neg c \in b$
126	124 125	nfan	$⊢ Ⅎ j ((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b)$
127		nfcv	$⊢ \underline{Ⅎ} j \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x}$
128		nfcv	$⊢ \underline{Ⅎ} j X$
129		nfcv	$⊢ \underline{Ⅎ} j b$
130	129	nfsum1	$⊢ \underline{Ⅎ} j \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A$
131	128 130	nfmpt	$⊢ \underline{Ⅎ} j (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
132	127 131	nfeq	$⊢ Ⅎ j \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
133	126 132	nfan	$⊢ Ⅎ j (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A))$
134		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ c / i ⦌ A$
135		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ c / j ⦌ C$
136		simpl	$⊢ (φ \land b \cup \{c\} \subseteq I) \to φ$
137	136	ad2antrr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to φ$
138	137 8	syl3an1	$⊢ ((((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land i \in I \land x \in X) \to A \in ℂ$
139	7	ad3antrrr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to I \in Fin$
140	89	adantl	$⊢ (φ \land b \cup \{c\} \subseteq I) \to b \subseteq I$
141	140	ad2antrr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to b \subseteq I$
142	139 141	ssfid	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to b \in Fin$
143		vex	$⊢ c \in V$
144	143	a1i	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to c \in V$
145		simplr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to \neg c \in b$
146		simpllr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to b \cup \{c\} \subseteq I$
147	5	ad3antrrr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to S \in \{ℝ, ℂ\}$
148	137	ad2antrr	$⊢ (((((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land x \in X) \land j \in b) \to φ$
149	141	ad2antrr	$⊢ (((((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land x \in X) \land j \in b) \to b \subseteq I$
150		simpr	$⊢ (((((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land x \in X) \land j \in b) \to j \in b$
151	149 150	sseldd	$⊢ (((((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land x \in X) \land j \in b) \to j \in I$
152		simplr	$⊢ (((((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land x \in X) \land j \in b) \to x \in X$
153		nfv	$⊢ Ⅎ i j \in I$
154		nfv	$⊢ Ⅎ i x \in X$
155	1 153 154	nf3an	$⊢ Ⅎ i (φ \land j \in I \land x \in X)$
156		nfv	$⊢ Ⅎ i C \in ℂ$
157	155 156	nfim	$⊢ Ⅎ i ((φ \land j \in I \land x \in X) \to C \in ℂ)$
158		eleq1w	$⊢ i = j \to (i \in I \leftrightarrow j \in I)$
159	158	3anbi2d	$⊢ i = j \to ((φ \land i \in I \land x \in X) \leftrightarrow (φ \land j \in I \land x \in X))$
160	11	eleq1d	$⊢ i = j \to (B \in ℂ \leftrightarrow C \in ℂ)$
161	159 160	imbi12d	$⊢ i = j \to (((φ \land i \in I \land x \in X) \to B \in ℂ) \leftrightarrow ((φ \land j \in I \land x \in X) \to C \in ℂ))$
162	157 161 9	chvarfv	$⊢ (φ \land j \in I \land x \in X) \to C \in ℂ$
163	148 151 152 162	syl3anc	$⊢ (((((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land x \in X) \land j \in b) \to C \in ℂ$
164		simpr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
165	136	adantr	$⊢ ((φ \land b \cup \{c\} \subseteq I) \land x \in X) \to φ$
166		id	$⊢ b \cup \{c\} \subseteq I \to b \cup \{c\} \subseteq I$
167		vsnid	$⊢ c \in \{c\}$
168		elun2	$⊢ c \in \{c\} \to c \in (b \cup \{c\})$
169	167 168	mp1i	$⊢ b \cup \{c\} \subseteq I \to c \in (b \cup \{c\})$
170	166 169	sseldd	$⊢ b \cup \{c\} \subseteq I \to c \in I$
171	170	ad2antlr	$⊢ ((φ \land b \cup \{c\} \subseteq I) \land x \in X) \to c \in I$
172		simpr	$⊢ ((φ \land b \cup \{c\} \subseteq I) \land x \in X) \to x \in X$
173		nfv	$⊢ Ⅎ j c \in I$
174		nfv	$⊢ Ⅎ j x \in X$
175	2 173 174	nf3an	$⊢ Ⅎ j (φ \land c \in I \land x \in X)$
176	135	nfel1	$⊢ Ⅎ j ⦋ c / j ⦌ C \in ℂ$
177	175 176	nfim	$⊢ Ⅎ j ((φ \land c \in I \land x \in X) \to ⦋ c / j ⦌ C \in ℂ)$
178		eleq1w	$⊢ j = c \to (j \in I \leftrightarrow c \in I)$
179	178	3anbi2d	$⊢ j = c \to ((φ \land j \in I \land x \in X) \leftrightarrow (φ \land c \in I \land x \in X))$
180		csbeq1a	$⊢ j = c \to C = ⦋ c / j ⦌ C$
181	180	eleq1d	$⊢ j = c \to (C \in ℂ \leftrightarrow ⦋ c / j ⦌ C \in ℂ)$
182	179 181	imbi12d	$⊢ j = c \to (((φ \land j \in I \land x \in X) \to C \in ℂ) \leftrightarrow ((φ \land c \in I \land x \in X) \to ⦋ c / j ⦌ C \in ℂ))$
183	177 182 162	chvarfv	$⊢ (φ \land c \in I \land x \in X) \to ⦋ c / j ⦌ C \in ℂ$
184	165 171 172 183	syl3anc	$⊢ ((φ \land b \cup \{c\} \subseteq I) \land x \in X) \to ⦋ c / j ⦌ C \in ℂ$
185	184	ad4ant14	$⊢ ((((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land x \in X) \to ⦋ c / j ⦌ C \in ℂ$
186	2 173	nfan	$⊢ Ⅎ j (φ \land c \in I)$
187		nfcv	$⊢ \underline{Ⅎ} j \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x}$
188	128 135	nfmpt	$⊢ \underline{Ⅎ} j (x \in X ⟼ ⦋ c / j ⦌ C)$
189	187 188	nfeq	$⊢ Ⅎ j \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C)$
190	186 189	nfim	$⊢ Ⅎ j ((φ \land c \in I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C))$
191	178	anbi2d	$⊢ j = c \to ((φ \land j \in I) \leftrightarrow (φ \land c \in I))$
192		csbeq1	$⊢ j = c \to ⦋ j / i ⦌ A = ⦋ c / i ⦌ A$
193	192	mpteq2dv	$⊢ j = c \to (x \in X ⟼ ⦋ j / i ⦌ A) = (x \in X ⟼ ⦋ c / i ⦌ A)$
194	193	oveq2d	$⊢ j = c \to \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x}$
195	180	mpteq2dv	$⊢ j = c \to (x \in X ⟼ C) = (x \in X ⟼ ⦋ c / j ⦌ C)$
196	194 195	eqeq12d	$⊢ j = c \to (\frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C) \leftrightarrow \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C))$
197	191 196	imbi12d	$⊢ j = c \to (((φ \land j \in I) \to \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C)) \leftrightarrow ((φ \land c \in I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C)))$
198	1 153	nfan	$⊢ Ⅎ i (φ \land j \in I)$
199		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ j / i ⦌ A$
200	109 199	nfmpt	$⊢ \underline{Ⅎ} i (x \in X ⟼ ⦋ j / i ⦌ A)$
201	107 108 200	nfov	$⊢ \underline{Ⅎ} i \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x}$
202		nfcv	$⊢ \underline{Ⅎ} i (x \in X ⟼ C)$
203	201 202	nfeq	$⊢ Ⅎ i \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C)$
204	198 203	nfim	$⊢ Ⅎ i ((φ \land j \in I) \to \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C))$
205	158	anbi2d	$⊢ i = j \to ((φ \land i \in I) \leftrightarrow (φ \land j \in I))$
206		csbeq1a	$⊢ i = j \to A = ⦋ j / i ⦌ A$
207	206	mpteq2dv	$⊢ i = j \to (x \in X ⟼ A) = (x \in X ⟼ ⦋ j / i ⦌ A)$
208	207	oveq2d	$⊢ i = j \to \frac{d (x \in X⟼ A)}{d_{S} x} = \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x}$
209	11	mpteq2dv	$⊢ i = j \to (x \in X ⟼ B) = (x \in X ⟼ C)$
210	208 209	eqeq12d	$⊢ i = j \to (\frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B) \leftrightarrow \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C))$
211	205 210	imbi12d	$⊢ i = j \to (((φ \land i \in I) \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ B)) \leftrightarrow ((φ \land j \in I) \to \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C)))$
212	204 211 10	chvarfv	$⊢ (φ \land j \in I) \to \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C)$
213	190 197 212	chvarfv	$⊢ (φ \land c \in I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C)$
214	170 213	sylan2	$⊢ (φ \land b \cup \{c\} \subseteq I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C)$
215	214	ad2antrr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C)$
216		csbeq1a	$⊢ i = c \to A = ⦋ c / i ⦌ A$
217	102 122 133 134 135 138 142 144 145 146 147 163 164 185 215 216 180	dvmptfprodlem	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to \frac{d (x \in X⟼ \prod_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b \cup \{c\}} C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A)$
218	85 86 94 217	syl21anc	$⊢ ((b \in Fin \land \neg c \in b) \land ((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \land (φ \land b \cup \{c\} \subseteq I)) \to \frac{d (x \in X⟼ \prod_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b \cup \{c\}} C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A)$
219	218	3exp	$⊢ (b \in Fin \land \neg c \in b) \to (((φ \land b \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)) \to ((φ \land b \cup \{c\} \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in b \cup \{c\}} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in b \cup \{c\}} C \prod_{i \in (b \cup \{c\}) ∖ \{j\}} A)))$
220	27 41 55 69 84 219	findcard2s	$⊢ I \in Fin \to ((φ \land I \subseteq I) \to \frac{d (x \in X⟼ \prod_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in I} C \prod_{i \in I ∖ \{j\}} A))$
221	7 13 220	sylc	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in I} A)}{d_{S} x} = (x \in X ⟼ \sum_{j \in I} C \prod_{i \in I ∖ \{j\}} A)$

Metamath Proof Explorer

Theorem dvmptfprod

Proof