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 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 ) ) )