Metamath Proof Explorer

Theorem evlsbagval

Description: Polynomial evaluation builder for a bag of variables. EDITORIAL: This theorem should stay in my mathbox until there's another use, since .0. and .1. using U instead of S is convenient for its sole use case mhphf , but may not be convenient for other uses. (Contributed by SN, 29-Jul-2024)

Ref Expression
Hypotheses evlsbagval.q 
|- Q = ( ( I evalSub S ) ` R )
evlsbagval.p 
|- P = ( I mPoly U )
evlsbagval.u 
|- U = ( S |`s R )
evlsbagval.w 
|- W = ( Base ` P )
evlsbagval.k 
|- K = ( Base ` S )
evlsbagval.m 
|- M = ( mulGrp ` S )
evlsbagval.e 
|- .^ = ( .g ` M )
evlsbagval.z 
|- .0. = ( 0g ` U )
evlsbagval.o 
|- .1. = ( 1r ` U )
evlsbagval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlsbagval.f 
|- F = ( s e. D |-> if ( s = B , .1. , .0. ) )
evlsbagval.i 
|- ( ph -> I e. V )
evlsbagval.s 
|- ( ph -> S e. CRing )
evlsbagval.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsbagval.a 
|- ( ph -> A e. ( K ^m I ) )
evlsbagval.b 
|- ( ph -> B e. D )
Assertion evlsbagval 
|- ( ph -> ( F e. W /\ ( ( Q ` F ) ` A ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 evlsbagval.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsbagval.p 
 |-  P = ( I mPoly U )
3 evlsbagval.u 
 |-  U = ( S |`s R )
4 evlsbagval.w 
 |-  W = ( Base ` P )
5 evlsbagval.k 
 |-  K = ( Base ` S )
6 evlsbagval.m 
 |-  M = ( mulGrp ` S )
7 evlsbagval.e 
 |-  .^ = ( .g ` M )
8 evlsbagval.z 
 |-  .0. = ( 0g ` U )
9 evlsbagval.o 
 |-  .1. = ( 1r ` U )
10 evlsbagval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
11 evlsbagval.f 
 |-  F = ( s e. D |-> if ( s = B , .1. , .0. ) )
12 evlsbagval.i 
 |-  ( ph -> I e. V )
13 evlsbagval.s 
 |-  ( ph -> S e. CRing )
14 evlsbagval.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
15 evlsbagval.a 
 |-  ( ph -> A e. ( K ^m I ) )
16 evlsbagval.b 
 |-  ( ph -> B e. D )
17 fvexd 
 |-  ( ph -> ( Base ` U ) e. _V )
18 ovexd 
 |-  ( ph -> ( NN0 ^m I ) e. _V )
19 10 18 rabexd 
 |-  ( ph -> D e. _V )
20 3 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
21 14 20 syl 
 |-  ( ph -> U e. Ring )
22 eqid 
 |-  ( Base ` U ) = ( Base ` U )
23 22 9 ringidcl 
 |-  ( U e. Ring -> .1. e. ( Base ` U ) )
24 21 23 syl 
 |-  ( ph -> .1. e. ( Base ` U ) )
25 22 8 ring0cl 
 |-  ( U e. Ring -> .0. e. ( Base ` U ) )
26 21 25 syl 
 |-  ( ph -> .0. e. ( Base ` U ) )
27 24 26 ifcld 
 |-  ( ph -> if ( s = B , .1. , .0. ) e. ( Base ` U ) )
28 27 adantr 
 |-  ( ( ph /\ s e. D ) -> if ( s = B , .1. , .0. ) e. ( Base ` U ) )
29 28 11 fmptd 
 |-  ( ph -> F : D --> ( Base ` U ) )
30 17 19 29 elmapdd 
 |-  ( ph -> F e. ( ( Base ` U ) ^m D ) )
31 eqid 
 |-  ( I mPwSer U ) = ( I mPwSer U )
32 eqid 
 |-  ( Base ` ( I mPwSer U ) ) = ( Base ` ( I mPwSer U ) )
33 31 22 10 32 12 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer U ) ) = ( ( Base ` U ) ^m D ) )
34 30 33 eleqtrrd 
 |-  ( ph -> F e. ( Base ` ( I mPwSer U ) ) )
35 19 26 11 sniffsupp 
 |-  ( ph -> F finSupp .0. )
36 2 31 32 8 4 mplelbas 
 |-  ( F e. W <-> ( F e. ( Base ` ( I mPwSer U ) ) /\ F finSupp .0. ) )
37 34 35 36 sylanbrc 
 |-  ( ph -> F e. W )
38 fveq1 
 |-  ( p = F -> ( p ` b ) = ( F ` b ) )
39 38 fveq2d 
 |-  ( p = F -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( p ` b ) ) = ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) )
40 39 oveq1d 
 |-  ( p = F -> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( p ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) )
41 40 mpteq2dv 
 |-  ( p = F -> ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( p ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) = ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) )
42 41 oveq2d 
 |-  ( p = F -> ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( p ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) = ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) )
43 eqid 
 |-  ( S ^s ( K ^m I ) ) = ( S ^s ( K ^m I ) )
44 eqid 
 |-  ( mulGrp ` ( S ^s ( K ^m I ) ) ) = ( mulGrp ` ( S ^s ( K ^m I ) ) )
45 eqid 
 |-  ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) = ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) )
46 eqid 
 |-  ( .r ` ( S ^s ( K ^m I ) ) ) = ( .r ` ( S ^s ( K ^m I ) ) )
47 eqid 
 |-  ( p e. W |-> ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( p ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) ) = ( p e. W |-> ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( p ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) )
48 eqid 
 |-  ( x e. R |-> ( ( K ^m I ) X. { x } ) ) = ( x e. R |-> ( ( K ^m I ) X. { x } ) )
49 eqid 
 |-  ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) = ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) )
50 1 2 4 10 5 3 43 44 45 46 47 48 49 12 13 14 evlsval3 
 |-  ( ph -> Q = ( p e. W |-> ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( p ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) ) )
51 ovexd 
 |-  ( ph -> ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) e. _V )
52 42 50 37 51 fvmptd4 
 |-  ( ph -> ( Q ` F ) = ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) )
53 52 fveq1d 
 |-  ( ph -> ( ( Q ` F ) ` A ) = ( ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) ` A ) )
54 eqid 
 |-  ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( K ^m I ) ) )
55 eqid 
 |-  ( 0g ` ( S ^s ( K ^m I ) ) ) = ( 0g ` ( S ^s ( K ^m I ) ) )
56 13 crngringd 
 |-  ( ph -> S e. Ring )
57 ovexd 
 |-  ( ph -> ( K ^m I ) e. _V )
58 43 pwsring 
 |-  ( ( S e. Ring /\ ( K ^m I ) e. _V ) -> ( S ^s ( K ^m I ) ) e. Ring )
59 56 57 58 syl2anc 
 |-  ( ph -> ( S ^s ( K ^m I ) ) e. Ring )
60 59 ringcmnd 
 |-  ( ph -> ( S ^s ( K ^m I ) ) e. CMnd )
61 59 adantr 
 |-  ( ( ph /\ b e. D ) -> ( S ^s ( K ^m I ) ) e. Ring )
62 13 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ x e. R ) -> S e. CRing )
63 ovexd 
 |-  ( ( ( ph /\ b e. D ) /\ x e. R ) -> ( K ^m I ) e. _V )
64 5 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ K )
65 14 64 syl 
 |-  ( ph -> R C_ K )
66 65 adantr 
 |-  ( ( ph /\ b e. D ) -> R C_ K )
67 66 sselda 
 |-  ( ( ( ph /\ b e. D ) /\ x e. R ) -> x e. K )
68 fconst6g 
 |-  ( x e. K -> ( ( K ^m I ) X. { x } ) : ( K ^m I ) --> K )
69 67 68 syl 
 |-  ( ( ( ph /\ b e. D ) /\ x e. R ) -> ( ( K ^m I ) X. { x } ) : ( K ^m I ) --> K )
70 43 5 54 62 63 69 pwselbasr 
 |-  ( ( ( ph /\ b e. D ) /\ x e. R ) -> ( ( K ^m I ) X. { x } ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
71 70 fmpttd 
 |-  ( ( ph /\ b e. D ) -> ( x e. R |-> ( ( K ^m I ) X. { x } ) ) : R --> ( Base ` ( S ^s ( K ^m I ) ) ) )
72 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
73 3 72 subrg1 
 |-  ( R e. ( SubRing ` S ) -> ( 1r ` S ) = ( 1r ` U ) )
74 14 73 syl 
 |-  ( ph -> ( 1r ` S ) = ( 1r ` U ) )
75 72 subrg1cl 
 |-  ( R e. ( SubRing ` S ) -> ( 1r ` S ) e. R )
76 14 75 syl 
 |-  ( ph -> ( 1r ` S ) e. R )
77 74 76 eqeltrrd 
 |-  ( ph -> ( 1r ` U ) e. R )
78 9 77 eqeltrid 
 |-  ( ph -> .1. e. R )
79 3 subrgbas 
 |-  ( R e. ( SubRing ` S ) -> R = ( Base ` U ) )
80 14 79 syl 
 |-  ( ph -> R = ( Base ` U ) )
81 26 80 eleqtrrd 
 |-  ( ph -> .0. e. R )
82 78 81 ifcld 
 |-  ( ph -> if ( s = B , .1. , .0. ) e. R )
83 82 adantr 
 |-  ( ( ph /\ s e. D ) -> if ( s = B , .1. , .0. ) e. R )
84 83 11 fmptd 
 |-  ( ph -> F : D --> R )
85 84 ffvelrnda 
 |-  ( ( ph /\ b e. D ) -> ( F ` b ) e. R )
86 71 85 ffvelrnd 
 |-  ( ( ph /\ b e. D ) -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
87 44 54 mgpbas 
 |-  ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) )
88 43 pwscrng 
 |-  ( ( S e. CRing /\ ( K ^m I ) e. _V ) -> ( S ^s ( K ^m I ) ) e. CRing )
89 13 57 88 syl2anc 
 |-  ( ph -> ( S ^s ( K ^m I ) ) e. CRing )
90 44 crngmgp 
 |-  ( ( S ^s ( K ^m I ) ) e. CRing -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. CMnd )
91 89 90 syl 
 |-  ( ph -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. CMnd )
92 91 adantr 
 |-  ( ( ph /\ b e. D ) -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. CMnd )
93 simpr 
 |-  ( ( ph /\ b e. D ) -> b e. D )
94 13 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ x e. I ) -> S e. CRing )
95 ovexd 
 |-  ( ( ( ph /\ b e. D ) /\ x e. I ) -> ( K ^m I ) e. _V )
96 elmapi 
 |-  ( a e. ( K ^m I ) -> a : I --> K )
97 96 adantl 
 |-  ( ( ( ( ph /\ b e. D ) /\ x e. I ) /\ a e. ( K ^m I ) ) -> a : I --> K )
98 simplr 
 |-  ( ( ( ( ph /\ b e. D ) /\ x e. I ) /\ a e. ( K ^m I ) ) -> x e. I )
99 97 98 ffvelrnd 
 |-  ( ( ( ( ph /\ b e. D ) /\ x e. I ) /\ a e. ( K ^m I ) ) -> ( a ` x ) e. K )
100 99 fmpttd 
 |-  ( ( ( ph /\ b e. D ) /\ x e. I ) -> ( a e. ( K ^m I ) |-> ( a ` x ) ) : ( K ^m I ) --> K )
101 43 5 54 94 95 100 pwselbasr 
 |-  ( ( ( ph /\ b e. D ) /\ x e. I ) -> ( a e. ( K ^m I ) |-> ( a ` x ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
102 101 fmpttd 
 |-  ( ( ph /\ b e. D ) -> ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) : I --> ( Base ` ( S ^s ( K ^m I ) ) ) )
103 10 87 45 92 93 102 psrbagev2 
 |-  ( ( ph /\ b e. D ) -> ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
104 54 46 61 86 103 ringcld 
 |-  ( ( ph /\ b e. D ) -> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
105 104 fmpttd 
 |-  ( ph -> ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) : D --> ( Base ` ( S ^s ( K ^m I ) ) ) )
106 eqeq1 
 |-  ( s = b -> ( s = B <-> b = B ) )
107 106 ifbid 
 |-  ( s = b -> if ( s = B , .1. , .0. ) = if ( b = B , .1. , .0. ) )
108 eldifi 
 |-  ( b e. ( D \ { B } ) -> b e. D )
109 108 adantl 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> b e. D )
110 9 fvexi 
 |-  .1. e. _V
111 8 fvexi 
 |-  .0. e. _V
112 110 111 ifex 
 |-  if ( b = B , .1. , .0. ) e. _V
113 112 a1i 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> if ( b = B , .1. , .0. ) e. _V )
114 11 107 109 113 fvmptd3 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( F ` b ) = if ( b = B , .1. , .0. ) )
115 eldifsnneq 
 |-  ( b e. ( D \ { B } ) -> -. b = B )
116 115 adantl 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> -. b = B )
117 116 iffalsed 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> if ( b = B , .1. , .0. ) = .0. )
118 114 117 eqtrd 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( F ` b ) = .0. )
119 118 fveq2d 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) = ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` .0. ) )
120 sneq 
 |-  ( x = .0. -> { x } = { .0. } )
121 120 xpeq2d 
 |-  ( x = .0. -> ( ( K ^m I ) X. { x } ) = ( ( K ^m I ) X. { .0. } ) )
122 81 adantr 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> .0. e. R )
123 ovex 
 |-  ( K ^m I ) e. _V
124 snex 
 |-  { .0. } e. _V
125 123 124 xpex 
 |-  ( ( K ^m I ) X. { .0. } ) e. _V
126 125 a1i 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( K ^m I ) X. { .0. } ) e. _V )
127 48 121 122 126 fvmptd3 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` .0. ) = ( ( K ^m I ) X. { .0. } ) )
128 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
129 3 128 subrg0 
 |-  ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
130 14 129 syl 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` U ) )
131 130 8 eqtr4di 
 |-  ( ph -> ( 0g ` S ) = .0. )
132 131 sneqd 
 |-  ( ph -> { ( 0g ` S ) } = { .0. } )
133 132 xpeq2d 
 |-  ( ph -> ( ( K ^m I ) X. { ( 0g ` S ) } ) = ( ( K ^m I ) X. { .0. } ) )
134 56 ringgrpd 
 |-  ( ph -> S e. Grp )
135 134 grpmndd 
 |-  ( ph -> S e. Mnd )
136 43 128 pws0g 
 |-  ( ( S e. Mnd /\ ( K ^m I ) e. _V ) -> ( ( K ^m I ) X. { ( 0g ` S ) } ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
137 135 57 136 syl2anc 
 |-  ( ph -> ( ( K ^m I ) X. { ( 0g ` S ) } ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
138 133 137 eqtr3d 
 |-  ( ph -> ( ( K ^m I ) X. { .0. } ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
139 138 adantr 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( K ^m I ) X. { .0. } ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
140 119 127 139 3eqtrd 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
141 140 oveq1d 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( ( 0g ` ( S ^s ( K ^m I ) ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) )
142 91 adantr 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. CMnd )
143 13 ad2antrr 
 |-  ( ( ( ph /\ b e. ( D \ { B } ) ) /\ x e. I ) -> S e. CRing )
144 ovexd 
 |-  ( ( ( ph /\ b e. ( D \ { B } ) ) /\ x e. I ) -> ( K ^m I ) e. _V )
145 96 adantl 
 |-  ( ( ( ( ph /\ b e. ( D \ { B } ) ) /\ x e. I ) /\ a e. ( K ^m I ) ) -> a : I --> K )
146 simplr 
 |-  ( ( ( ( ph /\ b e. ( D \ { B } ) ) /\ x e. I ) /\ a e. ( K ^m I ) ) -> x e. I )
147 145 146 ffvelrnd 
 |-  ( ( ( ( ph /\ b e. ( D \ { B } ) ) /\ x e. I ) /\ a e. ( K ^m I ) ) -> ( a ` x ) e. K )
148 147 fmpttd 
 |-  ( ( ( ph /\ b e. ( D \ { B } ) ) /\ x e. I ) -> ( a e. ( K ^m I ) |-> ( a ` x ) ) : ( K ^m I ) --> K )
149 43 5 54 143 144 148 pwselbasr 
 |-  ( ( ( ph /\ b e. ( D \ { B } ) ) /\ x e. I ) -> ( a e. ( K ^m I ) |-> ( a ` x ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
150 149 fmpttd 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) : I --> ( Base ` ( S ^s ( K ^m I ) ) ) )
151 10 87 45 142 109 150 psrbagev2 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
152 54 46 55 ringlz 
 |-  ( ( ( S ^s ( K ^m I ) ) e. Ring /\ ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) ) -> ( ( 0g ` ( S ^s ( K ^m I ) ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
153 59 151 152 syl2an2r 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( 0g ` ( S ^s ( K ^m I ) ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
154 141 153 eqtrd 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
155 154 19 suppss2 
 |-  ( ph -> ( ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) supp ( 0g ` ( S ^s ( K ^m I ) ) ) ) C_ { B } )
156 19 mptexd 
 |-  ( ph -> ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) e. _V )
157 fvexd 
 |-  ( ph -> ( 0g ` ( S ^s ( K ^m I ) ) ) e. _V )
158 funmpt 
 |-  Fun ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) )
159 158 a1i 
 |-  ( ph -> Fun ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) )
160 snfi 
 |-  { B } e. Fin
161 160 a1i 
 |-  ( ph -> { B } e. Fin )
162 161 155 ssfid 
 |-  ( ph -> ( ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) supp ( 0g ` ( S ^s ( K ^m I ) ) ) ) e. Fin )
163 156 157 159 162 isfsuppd 
 |-  ( ph -> ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) finSupp ( 0g ` ( S ^s ( K ^m I ) ) ) )
164 54 55 60 19 105 155 163 gsumres 
 |-  ( ph -> ( ( S ^s ( K ^m I ) ) gsum ( ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) |` { B } ) ) = ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) )
165 16 snssd 
 |-  ( ph -> { B } C_ D )
166 165 resmptd 
 |-  ( ph -> ( ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) |` { B } ) = ( b e. { B } |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) )
167 166 oveq2d 
 |-  ( ph -> ( ( S ^s ( K ^m I ) ) gsum ( ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) |` { B } ) ) = ( ( S ^s ( K ^m I ) ) gsum ( b e. { B } |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) )
168 164 167 eqtr3d 
 |-  ( ph -> ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) = ( ( S ^s ( K ^m I ) ) gsum ( b e. { B } |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) )
169 168 fveq1d 
 |-  ( ph -> ( ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) ` A ) = ( ( ( S ^s ( K ^m I ) ) gsum ( b e. { B } |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) ` A ) )
170 fveq1 
 |-  ( g = A -> ( g ` v ) = ( A ` v ) )
171 170 oveq2d 
 |-  ( g = A -> ( ( B ` v ) .^ ( g ` v ) ) = ( ( B ` v ) .^ ( A ` v ) ) )
172 171 mpteq2dv 
 |-  ( g = A -> ( v e. I |-> ( ( B ` v ) .^ ( g ` v ) ) ) = ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) )
173 172 oveq2d 
 |-  ( g = A -> ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) )
174 59 ringgrpd 
 |-  ( ph -> ( S ^s ( K ^m I ) ) e. Grp )
175 174 grpmndd 
 |-  ( ph -> ( S ^s ( K ^m I ) ) e. Mnd )
176 iftrue 
 |-  ( s = B -> if ( s = B , .1. , .0. ) = .1. )
177 110 a1i 
 |-  ( ph -> .1. e. _V )
178 11 176 16 177 fvmptd3 
 |-  ( ph -> ( F ` B ) = .1. )
179 178 fveq2d 
 |-  ( ph -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) = ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` .1. ) )
180 9 74 eqtr4id 
 |-  ( ph -> .1. = ( 1r ` S ) )
181 180 fveq2d 
 |-  ( ph -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` .1. ) = ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( 1r ` S ) ) )
182 sneq 
 |-  ( x = ( 1r ` S ) -> { x } = { ( 1r ` S ) } )
183 182 xpeq2d 
 |-  ( x = ( 1r ` S ) -> ( ( K ^m I ) X. { x } ) = ( ( K ^m I ) X. { ( 1r ` S ) } ) )
184 snex 
 |-  { ( 1r ` S ) } e. _V
185 184 a1i 
 |-  ( ph -> { ( 1r ` S ) } e. _V )
186 57 185 xpexd 
 |-  ( ph -> ( ( K ^m I ) X. { ( 1r ` S ) } ) e. _V )
187 48 183 76 186 fvmptd3 
 |-  ( ph -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( 1r ` S ) ) = ( ( K ^m I ) X. { ( 1r ` S ) } ) )
188 181 187 eqtrd 
 |-  ( ph -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` .1. ) = ( ( K ^m I ) X. { ( 1r ` S ) } ) )
189 43 72 pws1 
 |-  ( ( S e. Ring /\ ( K ^m I ) e. _V ) -> ( ( K ^m I ) X. { ( 1r ` S ) } ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
190 56 57 189 syl2anc 
 |-  ( ph -> ( ( K ^m I ) X. { ( 1r ` S ) } ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
191 179 188 190 3eqtrd 
 |-  ( ph -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
192 191 oveq1d 
 |-  ( ph -> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( ( 1r ` ( S ^s ( K ^m I ) ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) )
193 13 adantr 
 |-  ( ( ph /\ x e. I ) -> S e. CRing )
194 ovexd 
 |-  ( ( ph /\ x e. I ) -> ( K ^m I ) e. _V )
195 96 adantl 
 |-  ( ( ( ph /\ x e. I ) /\ a e. ( K ^m I ) ) -> a : I --> K )
196 simplr 
 |-  ( ( ( ph /\ x e. I ) /\ a e. ( K ^m I ) ) -> x e. I )
197 195 196 ffvelrnd 
 |-  ( ( ( ph /\ x e. I ) /\ a e. ( K ^m I ) ) -> ( a ` x ) e. K )
198 197 fmpttd 
 |-  ( ( ph /\ x e. I ) -> ( a e. ( K ^m I ) |-> ( a ` x ) ) : ( K ^m I ) --> K )
199 43 5 54 193 194 198 pwselbasr 
 |-  ( ( ph /\ x e. I ) -> ( a e. ( K ^m I ) |-> ( a ` x ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
200 199 fmpttd 
 |-  ( ph -> ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) : I --> ( Base ` ( S ^s ( K ^m I ) ) ) )
201 10 87 45 91 16 200 psrbagev2 
 |-  ( ph -> ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
202 eqid 
 |-  ( 1r ` ( S ^s ( K ^m I ) ) ) = ( 1r ` ( S ^s ( K ^m I ) ) )
203 54 46 202 ringlidm 
 |-  ( ( ( S ^s ( K ^m I ) ) e. Ring /\ ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) ) -> ( ( 1r ` ( S ^s ( K ^m I ) ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) )
204 59 201 203 syl2anc 
 |-  ( ph -> ( ( 1r ` ( S ^s ( K ^m I ) ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) )
205 192 204 eqtrd 
 |-  ( ph -> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) )
206 205 201 eqeltrd 
 |-  ( ph -> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
207 2fveq3 
 |-  ( b = B -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) = ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) )
208 oveq1 
 |-  ( b = B -> ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) = ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) )
209 208 oveq2d 
 |-  ( b = B -> ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) = ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) )
210 207 209 oveq12d 
 |-  ( b = B -> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) )
211 54 210 gsumsn 
 |-  ( ( ( S ^s ( K ^m I ) ) e. Mnd /\ B e. D /\ ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) ) -> ( ( S ^s ( K ^m I ) ) gsum ( b e. { B } |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) = ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) )
212 175 16 206 211 syl3anc 
 |-  ( ph -> ( ( S ^s ( K ^m I ) ) gsum ( b e. { B } |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) = ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` B ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) )
213 10 psrbagf 
 |-  ( B e. D -> B : I --> NN0 )
214 16 213 syl 
 |-  ( ph -> B : I --> NN0 )
215 214 ffnd 
 |-  ( ph -> B Fn I )
216 123 mptex 
 |-  ( a e. ( K ^m I ) |-> ( a ` x ) ) e. _V
217 216 49 fnmpti 
 |-  ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) Fn I
218 217 a1i 
 |-  ( ph -> ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) Fn I )
219 inidm 
 |-  ( I i^i I ) = I
220 eqidd 
 |-  ( ( ph /\ v e. I ) -> ( B ` v ) = ( B ` v ) )
221 fveq2 
 |-  ( x = v -> ( a ` x ) = ( a ` v ) )
222 221 mpteq2dv 
 |-  ( x = v -> ( a e. ( K ^m I ) |-> ( a ` x ) ) = ( a e. ( K ^m I ) |-> ( a ` v ) ) )
223 simpr 
 |-  ( ( ph /\ v e. I ) -> v e. I )
224 123 mptex 
 |-  ( a e. ( K ^m I ) |-> ( a ` v ) ) e. _V
225 224 a1i 
 |-  ( ( ph /\ v e. I ) -> ( a e. ( K ^m I ) |-> ( a ` v ) ) e. _V )
226 49 222 223 225 fvmptd3 
 |-  ( ( ph /\ v e. I ) -> ( ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ` v ) = ( a e. ( K ^m I ) |-> ( a ` v ) ) )
227 215 218 12 12 219 220 226 offval 
 |-  ( ph -> ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) = ( v e. I |-> ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) ) )
228 13 adantr 
 |-  ( ( ph /\ v e. I ) -> S e. CRing )
229 ovexd 
 |-  ( ( ph /\ v e. I ) -> ( K ^m I ) e. _V )
230 44 ringmgp 
 |-  ( ( S ^s ( K ^m I ) ) e. Ring -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. Mnd )
231 59 230 syl 
 |-  ( ph -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. Mnd )
232 231 adantr 
 |-  ( ( ph /\ v e. I ) -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. Mnd )
233 214 ffvelrnda 
 |-  ( ( ph /\ v e. I ) -> ( B ` v ) e. NN0 )
234 96 adantl 
 |-  ( ( ( ph /\ v e. I ) /\ a e. ( K ^m I ) ) -> a : I --> K )
235 simplr 
 |-  ( ( ( ph /\ v e. I ) /\ a e. ( K ^m I ) ) -> v e. I )
236 234 235 ffvelrnd 
 |-  ( ( ( ph /\ v e. I ) /\ a e. ( K ^m I ) ) -> ( a ` v ) e. K )
237 236 fmpttd 
 |-  ( ( ph /\ v e. I ) -> ( a e. ( K ^m I ) |-> ( a ` v ) ) : ( K ^m I ) --> K )
238 43 5 54 228 229 237 pwselbasr 
 |-  ( ( ph /\ v e. I ) -> ( a e. ( K ^m I ) |-> ( a ` v ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
239 87 45 mulgnn0cl 
 |-  ( ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. Mnd /\ ( B ` v ) e. NN0 /\ ( a e. ( K ^m I ) |-> ( a ` v ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) ) -> ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
240 232 233 238 239 syl3anc 
 |-  ( ( ph /\ v e. I ) -> ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
241 43 5 54 228 229 240 pwselbas 
 |-  ( ( ph /\ v e. I ) -> ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) : ( K ^m I ) --> K )
242 241 ffnd 
 |-  ( ( ph /\ v e. I ) -> ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) Fn ( K ^m I ) )
243 ovex 
 |-  ( ( B ` v ) .^ ( g ` v ) ) e. _V
244 eqid 
 |-  ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) = ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) )
245 243 244 fnmpti 
 |-  ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) Fn ( K ^m I )
246 245 a1i 
 |-  ( ( ph /\ v e. I ) -> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) Fn ( K ^m I ) )
247 eqid 
 |-  ( a e. ( K ^m I ) |-> ( a ` v ) ) = ( a e. ( K ^m I ) |-> ( a ` v ) )
248 fveq1 
 |-  ( a = l -> ( a ` v ) = ( l ` v ) )
249 simpr 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> l e. ( K ^m I ) )
250 fvexd 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( l ` v ) e. _V )
251 247 248 249 250 fvmptd3 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( ( a e. ( K ^m I ) |-> ( a ` v ) ) ` l ) = ( l ` v ) )
252 251 oveq2d 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( ( B ` v ) .^ ( ( a e. ( K ^m I ) |-> ( a ` v ) ) ` l ) ) = ( ( B ` v ) .^ ( l ` v ) ) )
253 56 ad2antrr 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> S e. Ring )
254 ovexd 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( K ^m I ) e. _V )
255 233 adantr 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( B ` v ) e. NN0 )
256 238 adantr 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( a e. ( K ^m I ) |-> ( a ` v ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
257 43 54 44 6 45 7 253 254 255 256 249 pwsexpg 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) ` l ) = ( ( B ` v ) .^ ( ( a e. ( K ^m I ) |-> ( a ` v ) ) ` l ) ) )
258 fveq1 
 |-  ( g = l -> ( g ` v ) = ( l ` v ) )
259 258 oveq2d 
 |-  ( g = l -> ( ( B ` v ) .^ ( g ` v ) ) = ( ( B ` v ) .^ ( l ` v ) ) )
260 ovexd 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( ( B ` v ) .^ ( l ` v ) ) e. _V )
261 244 259 249 260 fvmptd3 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ` l ) = ( ( B ` v ) .^ ( l ` v ) ) )
262 252 257 261 3eqtr4d 
 |-  ( ( ( ph /\ v e. I ) /\ l e. ( K ^m I ) ) -> ( ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) ` l ) = ( ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ` l ) )
263 242 246 262 eqfnfvd 
 |-  ( ( ph /\ v e. I ) -> ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) = ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) )
264 263 mpteq2dva 
 |-  ( ph -> ( v e. I |-> ( ( B ` v ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` v ) ) ) ) = ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) )
265 227 264 eqtrd 
 |-  ( ph -> ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) = ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) )
266 265 oveq2d 
 |-  ( ph -> ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) = ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) ) )
267 6 crngmgp 
 |-  ( S e. CRing -> M e. CMnd )
268 13 267 syl 
 |-  ( ph -> M e. CMnd )
269 268 cmnmndd 
 |-  ( ph -> M e. Mnd )
270 269 adantr 
 |-  ( ( ph /\ ( g e. ( K ^m I ) /\ v e. I ) ) -> M e. Mnd )
271 233 adantrl 
 |-  ( ( ph /\ ( g e. ( K ^m I ) /\ v e. I ) ) -> ( B ` v ) e. NN0 )
272 elmapi 
 |-  ( g e. ( K ^m I ) -> g : I --> K )
273 272 ad2antrl 
 |-  ( ( ph /\ ( g e. ( K ^m I ) /\ v e. I ) ) -> g : I --> K )
274 simprr 
 |-  ( ( ph /\ ( g e. ( K ^m I ) /\ v e. I ) ) -> v e. I )
275 273 274 ffvelrnd 
 |-  ( ( ph /\ ( g e. ( K ^m I ) /\ v e. I ) ) -> ( g ` v ) e. K )
276 6 5 mgpbas 
 |-  K = ( Base ` M )
277 276 7 mulgnn0cl 
 |-  ( ( M e. Mnd /\ ( B ` v ) e. NN0 /\ ( g ` v ) e. K ) -> ( ( B ` v ) .^ ( g ` v ) ) e. K )
278 270 271 275 277 syl3anc 
 |-  ( ( ph /\ ( g e. ( K ^m I ) /\ v e. I ) ) -> ( ( B ` v ) .^ ( g ` v ) ) e. K )
279 12 mptexd 
 |-  ( ph -> ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) e. _V )
280 fvexd 
 |-  ( ph -> ( 1r ` ( S ^s ( K ^m I ) ) ) e. _V )
281 funmpt 
 |-  Fun ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) )
282 281 a1i 
 |-  ( ph -> Fun ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) )
283 10 psrbagfsupp 
 |-  ( B e. D -> B finSupp 0 )
284 16 283 syl 
 |-  ( ph -> B finSupp 0 )
285 284 fsuppimpd 
 |-  ( ph -> ( B supp 0 ) e. Fin )
286 ssidd 
 |-  ( ph -> ( B supp 0 ) C_ ( B supp 0 ) )
287 c0ex 
 |-  0 e. _V
288 287 a1i 
 |-  ( ph -> 0 e. _V )
289 214 286 12 288 suppssr 
 |-  ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( B ` v ) = 0 )
290 289 oveq1d 
 |-  ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( ( B ` v ) .^ ( g ` v ) ) = ( 0 .^ ( g ` v ) ) )
291 290 adantr 
 |-  ( ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) /\ g e. ( K ^m I ) ) -> ( ( B ` v ) .^ ( g ` v ) ) = ( 0 .^ ( g ` v ) ) )
292 272 adantl 
 |-  ( ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) /\ g e. ( K ^m I ) ) -> g : I --> K )
293 eldifi 
 |-  ( v e. ( I \ ( B supp 0 ) ) -> v e. I )
294 293 ad2antlr 
 |-  ( ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) /\ g e. ( K ^m I ) ) -> v e. I )
295 292 294 ffvelrnd 
 |-  ( ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) /\ g e. ( K ^m I ) ) -> ( g ` v ) e. K )
296 6 72 ringidval 
 |-  ( 1r ` S ) = ( 0g ` M )
297 276 296 7 mulg0 
 |-  ( ( g ` v ) e. K -> ( 0 .^ ( g ` v ) ) = ( 1r ` S ) )
298 295 297 syl 
 |-  ( ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) /\ g e. ( K ^m I ) ) -> ( 0 .^ ( g ` v ) ) = ( 1r ` S ) )
299 291 298 eqtrd 
 |-  ( ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) /\ g e. ( K ^m I ) ) -> ( ( B ` v ) .^ ( g ` v ) ) = ( 1r ` S ) )
300 299 mpteq2dva 
 |-  ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) = ( g e. ( K ^m I ) |-> ( 1r ` S ) ) )
301 fconstmpt 
 |-  ( ( K ^m I ) X. { ( 1r ` S ) } ) = ( g e. ( K ^m I ) |-> ( 1r ` S ) )
302 ovexd 
 |-  ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( K ^m I ) e. _V )
303 56 302 189 syl2an2r 
 |-  ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( ( K ^m I ) X. { ( 1r ` S ) } ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
304 301 303 eqtr3id 
 |-  ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( g e. ( K ^m I ) |-> ( 1r ` S ) ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
305 300 304 eqtrd 
 |-  ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
306 305 12 suppss2 
 |-  ( ph -> ( ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) supp ( 1r ` ( S ^s ( K ^m I ) ) ) ) C_ ( B supp 0 ) )
307 285 306 ssfid 
 |-  ( ph -> ( ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) supp ( 1r ` ( S ^s ( K ^m I ) ) ) ) e. Fin )
308 279 280 282 307 isfsuppd 
 |-  ( ph -> ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) finSupp ( 1r ` ( S ^s ( K ^m I ) ) ) )
309 43 5 202 44 6 57 12 13 278 308 pwsgprod 
 |-  ( ph -> ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( v e. I |-> ( g e. ( K ^m I ) |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) ) = ( g e. ( K ^m I ) |-> ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) ) )
310 204 266 309 3eqtrd 
 |-  ( ph -> ( ( 1r ` ( S ^s ( K ^m I ) ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( B oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) = ( g e. ( K ^m I ) |-> ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) ) )
311 212 192 310 3eqtrd 
 |-  ( ph -> ( ( S ^s ( K ^m I ) ) gsum ( b e. { B } |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) = ( g e. ( K ^m I ) |-> ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( g ` v ) ) ) ) ) )
312 ovexd 
 |-  ( ph -> ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) e. _V )
313 173 311 15 312 fvmptd4 
 |-  ( ph -> ( ( ( S ^s ( K ^m I ) ) gsum ( b e. { B } |-> ( ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) ( .r ` ( S ^s ( K ^m I ) ) ) ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) ) ) ) ) ` A ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) )
314 53 169 313 3eqtrd 
 |-  ( ph -> ( ( Q ` F ) ` A ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) )
315 37 314 jca 
 |-  ( ph -> ( F e. W /\ ( ( Q ` F ) ` A ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) )