dvmptfprod

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

	Ref	Expression
Hypotheses	dvmptfprod.iph	\|- F/ i ph
	dvmptfprod.jph	\|- F/ j ph
	dvmptfprod.j	\|- J = ( K \|`t S )
	dvmptfprod.k	\|- K = ( TopOpen ` CCfld )
	dvmptfprod.s	\|- ( ph -> S e. { RR , CC } )
	dvmptfprod.x	\|- ( ph -> X e. J )
	dvmptfprod.i	\|- ( ph -> I e. Fin )
	dvmptfprod.a	\|- ( ( ph /\ i e. I /\ x e. X ) -> A e. CC )
	dvmptfprod.b	\|- ( ( ph /\ i e. I /\ x e. X ) -> B e. CC )
	dvmptfprod.d	\|- ( ( ph /\ i e. I ) -> ( S _D ( x e. X \|-> A ) ) = ( x e. X \|-> B ) )
	dvmptfprod.bc	\|- ( i = j -> B = C )
Assertion	dvmptfprod	\|- ( ph -> ( S _D ( x e. X \|-> prod_ i e. I A ) ) = ( x e. X \|-> sum_ j e. I ( C x. prod_ i e. ( I \ { j } ) A ) ) )

Proof

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

Metamath Proof Explorer

Theorem dvmptfprod

Proof