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