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	a1d	$⊢ a = I \to (j \in I \to C \prod_{i \in a ∖ \{j\}} A = C \prod_{i \in I ∖ \{j\}} A)$
66	65	ralrimiv	$⊢ a = I \to \forall j \in I C \prod_{i \in a ∖ \{j\}} A = C \prod_{i \in I ∖ \{j\}} A$
67	66	sumeq2d	$⊢ 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$
68	61 67	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$
69	68	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)$
70	60 69	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))$
71	57 70	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)))$
72		prod0	$⊢ \prod_{i \in \emptyset} A = 1$
73	72	mpteq2i	$⊢ (x \in X ⟼ \prod_{i \in \emptyset} A) = (x \in X ⟼ 1)$
74	73	oveq2i	$⊢ \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x} = \frac{d (x \in X⟼ 1)}{d_{S} x}$
75	74	a1i	$⊢ φ \to \frac{d (x \in X⟼ \prod_{i \in \emptyset} A)}{d_{S} x} = \frac{d (x \in X⟼ 1)}{d_{S} x}$
76	4	oveq1i	$⊢ K ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
77	3 76	eqtri	$⊢ J = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
78	6 77	eleqtrdi	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
79		1cnd	$⊢ φ \to 1 \in ℂ$
80	5 78 79	dvmptconst	$⊢ φ \to \frac{d (x \in X⟼ 1)}{d_{S} x} = (x \in X ⟼ 0)$
81		sum0	$⊢ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A = 0$
82	81	eqcomi	$⊢ 0 = \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A$
83	82	mpteq2i	$⊢ (x \in X ⟼ 0) = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A)$
84	83	a1i	$⊢ φ \to (x \in X ⟼ 0) = (x \in X ⟼ \sum_{j \in \emptyset} C \prod_{i \in \emptyset ∖ \{j\}} A)$
85	75 80 84	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)$
86	85	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)$
87		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)$
88		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$
89		simpl	$⊢ (φ \land b \cup \{c\} \subseteq I) \to φ$
90		ssun1	$⊢ b \subseteq b \cup \{c\}$
91		sstr2	$⊢ b \subseteq b \cup \{c\} \to (b \cup \{c\} \subseteq I \to b \subseteq I)$
92	90 91	ax-mp	$⊢ b \cup \{c\} \subseteq I \to b \subseteq I$
93	92	adantl	$⊢ (φ \land b \cup \{c\} \subseteq I) \to b \subseteq I$
94	89 93	jca	$⊢ (φ \land b \cup \{c\} \subseteq I) \to (φ \land b \subseteq I)$
95	94	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)$
96		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))$
97	95 96	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)$
98	97	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)$
99		nfv	$⊢ Ⅎ x ((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b)$
100		nfcv	$⊢ \underline{Ⅎ} x S$
101		nfcv	$⊢ \underline{Ⅎ} x D$
102		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ \prod_{i \in b} A)$
103	100 101 102	nfov	$⊢ \underline{Ⅎ} x \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x}$
104		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
105	103 104	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)$
106	99 105	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))$
107		nfv	$⊢ Ⅎ i b \cup \{c\} \subseteq I$
108	1 107	nfan	$⊢ Ⅎ i (φ \land b \cup \{c\} \subseteq I)$
109		nfv	$⊢ Ⅎ i \neg c \in b$
110	108 109	nfan	$⊢ Ⅎ i ((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b)$
111		nfcv	$⊢ \underline{Ⅎ} i S$
112		nfcv	$⊢ \underline{Ⅎ} i D$
113		nfcv	$⊢ \underline{Ⅎ} i X$
114		nfcv	$⊢ \underline{Ⅎ} i b$
115	114	nfcprod1	$⊢ \underline{Ⅎ} i \prod_{i \in b} A$
116	113 115	nfmpt	$⊢ \underline{Ⅎ} i (x \in X ⟼ \prod_{i \in b} A)$
117	111 112 116	nfov	$⊢ \underline{Ⅎ} i \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x}$
118		nfcv	$⊢ \underline{Ⅎ} i C$
119		nfcv	$⊢ \underline{Ⅎ} i \times$
120		nfcv	$⊢ \underline{Ⅎ} i (b ∖ \{j\})$
121	120	nfcprod1	$⊢ \underline{Ⅎ} i \prod_{i \in b ∖ \{j\}} A$
122	118 119 121	nfov	$⊢ \underline{Ⅎ} i C \prod_{i \in b ∖ \{j\}} A$
123	114 122	nfsum	$⊢ \underline{Ⅎ} i \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A$
124	113 123	nfmpt	$⊢ \underline{Ⅎ} i (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
125	117 124	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)$
126	110 125	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))$
127		nfv	$⊢ Ⅎ j b \cup \{c\} \subseteq I$
128	2 127	nfan	$⊢ Ⅎ j (φ \land b \cup \{c\} \subseteq I)$
129		nfv	$⊢ Ⅎ j \neg c \in b$
130	128 129	nfan	$⊢ Ⅎ j ((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b)$
131		nfcv	$⊢ \underline{Ⅎ} j \frac{d (x \in X⟼ \prod_{i \in b} A)}{d_{S} x}$
132		nfcv	$⊢ \underline{Ⅎ} j X$
133		nfcv	$⊢ \underline{Ⅎ} j b$
134	133	nfsum1	$⊢ \underline{Ⅎ} j \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A$
135	132 134	nfmpt	$⊢ \underline{Ⅎ} j (x \in X ⟼ \sum_{j \in b} C \prod_{i \in b ∖ \{j\}} A)$
136	131 135	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)$
137	130 136	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))$
138		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ c / i ⦌ A$
139		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ c / j ⦌ C$
140	89	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 φ$
141	140	3ad2ant1	$⊢ ((((φ \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 φ$
142		simp2	$⊢ ((((φ \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 i \in I$
143		simp3	$⊢ ((((φ \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 x \in X$
144	141 142 143 8	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 i \in I \land x \in X) \to A \in ℂ$
145	140 7	syl	$⊢ (((φ \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$
146	93	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$
147		ssfi	$⊢ (I \in Fin \land b \subseteq I) \to b \in Fin$
148	145 146 147	syl2anc	$⊢ (((φ \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$
149		vex	$⊢ c \in V$
150	149	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$
151		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$
152		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$
153	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 \{ℝ, ℂ\}$
154	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)) \land x \in X) \land j \in b) \to φ$
155	146	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$
156		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$
157	155 156	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$
158		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$
159		nfv	$⊢ Ⅎ i j \in I$
160		nfv	$⊢ Ⅎ i x \in X$
161	1 159 160	nf3an	$⊢ Ⅎ i (φ \land j \in I \land x \in X)$
162		nfv	$⊢ Ⅎ i C \in ℂ$
163	161 162	nfim	$⊢ Ⅎ i ((φ \land j \in I \land x \in X) \to C \in ℂ)$
164		eleq1w	$⊢ i = j \to (i \in I \leftrightarrow j \in I)$
165	164	3anbi2d	$⊢ i = j \to ((φ \land i \in I \land x \in X) \leftrightarrow (φ \land j \in I \land x \in X))$
166	11	eleq1d	$⊢ i = j \to (B \in ℂ \leftrightarrow C \in ℂ)$
167	165 166	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 ℂ))$
168	163 167 9	chvarfv	$⊢ (φ \land j \in I \land x \in X) \to C \in ℂ$
169	154 157 158 168	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 ℂ$
170		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)$
171	89	adantr	$⊢ ((φ \land b \cup \{c\} \subseteq I) \land x \in X) \to φ$
172		id	$⊢ b \cup \{c\} \subseteq I \to b \cup \{c\} \subseteq I$
173	149	snid	$⊢ c \in \{c\}$
174		elun2	$⊢ c \in \{c\} \to c \in (b \cup \{c\})$
175	173 174	ax-mp	$⊢ c \in (b \cup \{c\})$
176	175	a1i	$⊢ b \cup \{c\} \subseteq I \to c \in (b \cup \{c\})$
177	172 176	sseldd	$⊢ b \cup \{c\} \subseteq I \to c \in I$
178	177	ad2antlr	$⊢ ((φ \land b \cup \{c\} \subseteq I) \land x \in X) \to c \in I$
179		simpr	$⊢ ((φ \land b \cup \{c\} \subseteq I) \land x \in X) \to x \in X$
180		nfv	$⊢ Ⅎ j c \in I$
181		nfv	$⊢ Ⅎ j x \in X$
182	2 180 181	nf3an	$⊢ Ⅎ j (φ \land c \in I \land x \in X)$
183		nfcv	$⊢ \underline{Ⅎ} j ℂ$
184	139 183	nfel	$⊢ Ⅎ j ⦋ c / j ⦌ C \in ℂ$
185	182 184	nfim	$⊢ Ⅎ j ((φ \land c \in I \land x \in X) \to ⦋ c / j ⦌ C \in ℂ)$
186		eleq1w	$⊢ j = c \to (j \in I \leftrightarrow c \in I)$
187	186	3anbi2d	$⊢ j = c \to ((φ \land j \in I \land x \in X) \leftrightarrow (φ \land c \in I \land x \in X))$
188		csbeq1a	$⊢ j = c \to C = ⦋ c / j ⦌ C$
189	188	eleq1d	$⊢ j = c \to (C \in ℂ \leftrightarrow ⦋ c / j ⦌ C \in ℂ)$
190	187 189	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 ℂ))$
191	185 190 168	chvarfv	$⊢ (φ \land c \in I \land x \in X) \to ⦋ c / j ⦌ C \in ℂ$
192	171 178 179 191	syl3anc	$⊢ ((φ \land b \cup \{c\} \subseteq I) \land x \in X) \to ⦋ c / j ⦌ C \in ℂ$
193	192	adantlr	$⊢ (((φ \land b \cup \{c\} \subseteq I) \land \neg c \in b) \land x \in X) \to ⦋ c / j ⦌ C \in ℂ$
194	193	adantlr	$⊢ ((((φ \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 ℂ$
195	2 180	nfan	$⊢ Ⅎ j (φ \land c \in I)$
196		nfcv	$⊢ \underline{Ⅎ} j \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x}$
197	132 139	nfmpt	$⊢ \underline{Ⅎ} j (x \in X ⟼ ⦋ c / j ⦌ C)$
198	196 197	nfeq	$⊢ Ⅎ j \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C)$
199	195 198	nfim	$⊢ Ⅎ j ((φ \land c \in I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C))$
200	186	anbi2d	$⊢ j = c \to ((φ \land j \in I) \leftrightarrow (φ \land c \in I))$
201		csbeq1a	$⊢ j = c \to ⦋ j / i ⦌ A = ⦋ c / j ⦌ ⦋ j / i ⦌ A$
202		csbcow	$⊢ ⦋ c / j ⦌ ⦋ j / i ⦌ A = ⦋ c / i ⦌ A$
203	202	a1i	$⊢ j = c \to ⦋ c / j ⦌ ⦋ j / i ⦌ A = ⦋ c / i ⦌ A$
204	201 203	eqtrd	$⊢ j = c \to ⦋ j / i ⦌ A = ⦋ c / i ⦌ A$
205	204	mpteq2dv	$⊢ j = c \to (x \in X ⟼ ⦋ j / i ⦌ A) = (x \in X ⟼ ⦋ c / i ⦌ A)$
206	205	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}$
207	188	mpteq2dv	$⊢ j = c \to (x \in X ⟼ C) = (x \in X ⟼ ⦋ c / j ⦌ C)$
208	206 207	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))$
209	200 208	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)))$
210	1 159	nfan	$⊢ Ⅎ i (φ \land j \in I)$
211		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ j / i ⦌ A$
212	113 211	nfmpt	$⊢ \underline{Ⅎ} i (x \in X ⟼ ⦋ j / i ⦌ A)$
213	111 112 212	nfov	$⊢ \underline{Ⅎ} i \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x}$
214		nfcv	$⊢ \underline{Ⅎ} i (x \in X ⟼ C)$
215	213 214	nfeq	$⊢ Ⅎ i \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C)$
216	210 215	nfim	$⊢ Ⅎ i ((φ \land j \in I) \to \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C))$
217	164	anbi2d	$⊢ i = j \to ((φ \land i \in I) \leftrightarrow (φ \land j \in I))$
218		csbeq1a	$⊢ i = j \to A = ⦋ j / i ⦌ A$
219	218	mpteq2dv	$⊢ i = j \to (x \in X ⟼ A) = (x \in X ⟼ ⦋ j / i ⦌ A)$
220	219	oveq2d	$⊢ i = j \to \frac{d (x \in X⟼ A)}{d_{S} x} = \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x}$
221	11	idi	$⊢ i = j \to B = C$
222	221	mpteq2dv	$⊢ i = j \to (x \in X ⟼ B) = (x \in X ⟼ C)$
223	220 222	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))$
224	217 223	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)))$
225	216 224 10	chvarfv	$⊢ (φ \land j \in I) \to \frac{d (x \in X⟼ ⦋ j / i ⦌ A)}{d_{S} x} = (x \in X ⟼ C)$
226	199 209 225	chvarfv	$⊢ (φ \land c \in I) \to \frac{d (x \in X⟼ ⦋ c / i ⦌ A)}{d_{S} x} = (x \in X ⟼ ⦋ c / j ⦌ C)$
227	177 226	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)$
228	227	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)$
229		csbeq1a	$⊢ i = c \to A = ⦋ c / i ⦌ A$
230	106 126 137 138 139 144 148 150 151 152 153 169 170 194 228 229 188	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)$
231	87 88 98 230	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)$
232	231	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)))$
233	27 41 55 71 86 232	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))$
234	7 13 233	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