Metamath Proof Explorer

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