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