Metamath Proof Explorer

Theorem evlsvvval

Description: Give a formula for the evaluation of a polynomial given assignments from variables to values. This is the sum of the evaluations for each term (corresponding to a bag of variables), that is, the coefficient times the product of each variable raised to the corresponding power. (Contributed by SN, 5-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 evlsvvval.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsvvval.p 
 |-  P = ( I mPoly U )
3 evlsvvval.b 
 |-  B = ( Base ` P )
4 evlsvvval.u 
 |-  U = ( S |`s R )
5 evlsvvval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6 evlsvvval.k 
 |-  K = ( Base ` S )
7 evlsvvval.m 
 |-  M = ( mulGrp ` S )
8 evlsvvval.w 
 |-  .^ = ( .g ` M )
9 evlsvvval.x 
 |-  .x. = ( .r ` S )
10 evlsvvval.i 
 |-  ( ph -> I e. V )
11 evlsvvval.s 
 |-  ( ph -> S e. CRing )
12 evlsvvval.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
13 evlsvvval.f 
 |-  ( ph -> F e. B )
14 evlsvvval.a 
 |-  ( ph -> A e. ( K ^m I ) )
15 fveq1 
 |-  ( l = A -> ( l ` i ) = ( A ` i ) )
16 15 oveq2d 
 |-  ( l = A -> ( ( b ` i ) .^ ( l ` i ) ) = ( ( b ` i ) .^ ( A ` i ) ) )
17 16 mpteq2dv 
 |-  ( l = A -> ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) = ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) )
18 17 oveq2d 
 |-  ( l = A -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) = ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) )
19 18 oveq2d 
 |-  ( l = A -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) = ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) )
20 19 mpteq2dv 
 |-  ( l = A -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) = ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) )
21 20 oveq2d 
 |-  ( l = A -> ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )
22 eqid 
 |-  ( S ^s ( K ^m I ) ) = ( S ^s ( K ^m I ) )
23 eqid 
 |-  ( mulGrp ` ( S ^s ( K ^m I ) ) ) = ( mulGrp ` ( S ^s ( K ^m I ) ) )
24 eqid 
 |-  ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) = ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) )
25 eqid 
 |-  ( .r ` ( S ^s ( K ^m I ) ) ) = ( .r ` ( S ^s ( K ^m I ) ) )
26 eqid 
 |-  ( x e. R |-> ( ( K ^m I ) X. { x } ) ) = ( x e. R |-> ( ( K ^m I ) X. { x } ) )
27 eqid 
 |-  ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) = ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) )
28 1 2 3 5 6 4 22 23 24 25 26 27 10 11 12 13 evlsvval 
 |-  ( 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 ) ) ) ) ) ) ) ) )
29 sneq 
 |-  ( x = ( F ` b ) -> { x } = { ( F ` b ) } )
30 29 xpeq2d 
 |-  ( x = ( F ` b ) -> ( ( K ^m I ) X. { x } ) = ( ( K ^m I ) X. { ( F ` b ) } ) )
31 eqid 
 |-  ( Base ` U ) = ( Base ` U )
32 2 31 3 5 13 mplelf 
 |-  ( ph -> F : D --> ( Base ` U ) )
33 4 subrgbas 
 |-  ( R e. ( SubRing ` S ) -> R = ( Base ` U ) )
34 12 33 syl 
 |-  ( ph -> R = ( Base ` U ) )
35 34 feq3d 
 |-  ( ph -> ( F : D --> R <-> F : D --> ( Base ` U ) ) )
36 32 35 mpbird 
 |-  ( ph -> F : D --> R )
37 36 ffvelcdmda 
 |-  ( ( ph /\ b e. D ) -> ( F ` b ) e. R )
38 ovex 
 |-  ( K ^m I ) e. _V
39 snex 
 |-  { ( F ` b ) } e. _V
40 38 39 xpex 
 |-  ( ( K ^m I ) X. { ( F ` b ) } ) e. _V
41 40 a1i 
 |-  ( ( ph /\ b e. D ) -> ( ( K ^m I ) X. { ( F ` b ) } ) e. _V )
42 26 30 37 41 fvmptd3 
 |-  ( ( ph /\ b e. D ) -> ( ( x e. R |-> ( ( K ^m I ) X. { x } ) ) ` ( F ` b ) ) = ( ( K ^m I ) X. { ( F ` b ) } ) )
43 5 psrbagf 
 |-  ( b e. D -> b : I --> NN0 )
44 43 adantl 
 |-  ( ( ph /\ b e. D ) -> b : I --> NN0 )
45 44 ffnd 
 |-  ( ( ph /\ b e. D ) -> b Fn I )
46 38 mptex 
 |-  ( a e. ( K ^m I ) |-> ( a ` x ) ) e. _V
47 46 27 fnmpti 
 |-  ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) Fn I
48 47 a1i 
 |-  ( ( ph /\ b e. D ) -> ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) Fn I )
49 10 adantr 
 |-  ( ( ph /\ b e. D ) -> I e. V )
50 inidm 
 |-  ( I i^i I ) = I
51 eqidd 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( b ` i ) = ( b ` i ) )
52 fveq2 
 |-  ( x = i -> ( a ` x ) = ( a ` i ) )
53 52 mpteq2dv 
 |-  ( x = i -> ( a e. ( K ^m I ) |-> ( a ` x ) ) = ( a e. ( K ^m I ) |-> ( a ` i ) ) )
54 simpr 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> i e. I )
55 eqid 
 |-  ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( K ^m I ) ) )
56 11 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> S e. CRing )
57 ovexd 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( K ^m I ) e. _V )
58 elmapi 
 |-  ( a e. ( K ^m I ) -> a : I --> K )
59 58 ffvelcdmda 
 |-  ( ( a e. ( K ^m I ) /\ i e. I ) -> ( a ` i ) e. K )
60 59 ancoms 
 |-  ( ( i e. I /\ a e. ( K ^m I ) ) -> ( a ` i ) e. K )
61 60 adantll 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ a e. ( K ^m I ) ) -> ( a ` i ) e. K )
62 61 fmpttd 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( a e. ( K ^m I ) |-> ( a ` i ) ) : ( K ^m I ) --> K )
63 22 6 55 56 57 62 pwselbasr 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( a e. ( K ^m I ) |-> ( a ` i ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
64 27 53 54 63 fvmptd3 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ` i ) = ( a e. ( K ^m I ) |-> ( a ` i ) ) )
65 45 48 49 49 50 51 64 offval 
 |-  ( ( ph /\ b e. D ) -> ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) = ( i e. I |-> ( ( b ` i ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` i ) ) ) ) )
66 23 55 mgpbas 
 |-  ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) )
67 11 crngringd 
 |-  ( ph -> S e. Ring )
68 ovexd 
 |-  ( ph -> ( K ^m I ) e. _V )
69 22 pwsring 
 |-  ( ( S e. Ring /\ ( K ^m I ) e. _V ) -> ( S ^s ( K ^m I ) ) e. Ring )
70 67 68 69 syl2anc 
 |-  ( ph -> ( S ^s ( K ^m I ) ) e. Ring )
71 23 ringmgp 
 |-  ( ( S ^s ( K ^m I ) ) e. Ring -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. Mnd )
72 70 71 syl 
 |-  ( ph -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. Mnd )
73 72 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( mulGrp ` ( S ^s ( K ^m I ) ) ) e. Mnd )
74 44 ffvelcdmda 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( b ` i ) e. NN0 )
75 66 24 73 74 63 mulgnn0cld 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( ( b ` i ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` i ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
76 22 6 55 56 57 75 pwselbas 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( ( b ` i ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` i ) ) ) : ( K ^m I ) --> K )
77 76 ffnd 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( ( b ` i ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` i ) ) ) Fn ( K ^m I ) )
78 ovex 
 |-  ( ( b ` i ) .^ ( m ` i ) ) e. _V
79 eqid 
 |-  ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) = ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) )
80 78 79 fnmpti 
 |-  ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) Fn ( K ^m I )
81 80 a1i 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) Fn ( K ^m I ) )
82 eqid 
 |-  ( a e. ( K ^m I ) |-> ( a ` i ) ) = ( a e. ( K ^m I ) |-> ( a ` i ) )
83 fveq1 
 |-  ( a = p -> ( a ` i ) = ( p ` i ) )
84 simpr 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> p e. ( K ^m I ) )
85 fvexd 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( p ` i ) e. _V )
86 82 83 84 85 fvmptd3 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( ( a e. ( K ^m I ) |-> ( a ` i ) ) ` p ) = ( p ` i ) )
87 86 oveq2d 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( ( b ` i ) .^ ( ( a e. ( K ^m I ) |-> ( a ` i ) ) ` p ) ) = ( ( b ` i ) .^ ( p ` i ) ) )
88 67 ad3antrrr 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> S e. Ring )
89 ovexd 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( K ^m I ) e. _V )
90 74 adantr 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( b ` i ) e. NN0 )
91 63 adantr 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( a e. ( K ^m I ) |-> ( a ` i ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
92 22 55 23 7 24 8 88 89 90 91 84 pwsexpg 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( ( ( b ` i ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` i ) ) ) ` p ) = ( ( b ` i ) .^ ( ( a e. ( K ^m I ) |-> ( a ` i ) ) ` p ) ) )
93 fveq1 
 |-  ( m = p -> ( m ` i ) = ( p ` i ) )
94 93 oveq2d 
 |-  ( m = p -> ( ( b ` i ) .^ ( m ` i ) ) = ( ( b ` i ) .^ ( p ` i ) ) )
95 ovexd 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( ( b ` i ) .^ ( p ` i ) ) e. _V )
96 79 94 84 95 fvmptd3 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ` p ) = ( ( b ` i ) .^ ( p ` i ) ) )
97 87 92 96 3eqtr4d 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. I ) /\ p e. ( K ^m I ) ) -> ( ( ( b ` i ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` i ) ) ) ` p ) = ( ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ` p ) )
98 77 81 97 eqfnfvd 
 |-  ( ( ( ph /\ b e. D ) /\ i e. I ) -> ( ( b ` i ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` i ) ) ) = ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) )
99 98 mpteq2dva 
 |-  ( ( ph /\ b e. D ) -> ( i e. I |-> ( ( b ` i ) ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( a e. ( K ^m I ) |-> ( a ` i ) ) ) ) = ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) )
100 65 99 eqtrd 
 |-  ( ( ph /\ b e. D ) -> ( b oF ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) ) ) = ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) )
101 100 oveq2d 
 |-  ( ( 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 ) ) ) ) ) = ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) )
102 eqid 
 |-  ( 1r ` ( S ^s ( K ^m I ) ) ) = ( 1r ` ( S ^s ( K ^m I ) ) )
103 ovexd 
 |-  ( ( ph /\ b e. D ) -> ( K ^m I ) e. _V )
104 11 adantr 
 |-  ( ( ph /\ b e. D ) -> S e. CRing )
105 7 6 mgpbas 
 |-  K = ( Base ` M )
106 7 ringmgp 
 |-  ( S e. Ring -> M e. Mnd )
107 67 106 syl 
 |-  ( ph -> M e. Mnd )
108 107 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ ( m e. ( K ^m I ) /\ i e. I ) ) -> M e. Mnd )
109 74 adantrl 
 |-  ( ( ( ph /\ b e. D ) /\ ( m e. ( K ^m I ) /\ i e. I ) ) -> ( b ` i ) e. NN0 )
110 elmapi 
 |-  ( m e. ( K ^m I ) -> m : I --> K )
111 110 ffvelcdmda 
 |-  ( ( m e. ( K ^m I ) /\ i e. I ) -> ( m ` i ) e. K )
112 111 adantl 
 |-  ( ( ( ph /\ b e. D ) /\ ( m e. ( K ^m I ) /\ i e. I ) ) -> ( m ` i ) e. K )
113 105 8 108 109 112 mulgnn0cld 
 |-  ( ( ( ph /\ b e. D ) /\ ( m e. ( K ^m I ) /\ i e. I ) ) -> ( ( b ` i ) .^ ( m ` i ) ) e. K )
114 49 mptexd 
 |-  ( ( ph /\ b e. D ) -> ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) e. _V )
115 fvexd 
 |-  ( ( ph /\ b e. D ) -> ( 1r ` ( S ^s ( K ^m I ) ) ) e. _V )
116 funmpt 
 |-  Fun ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) )
117 116 a1i 
 |-  ( ( ph /\ b e. D ) -> Fun ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) )
118 5 psrbagfsupp 
 |-  ( b e. D -> b finSupp 0 )
119 118 adantl 
 |-  ( ( ph /\ b e. D ) -> b finSupp 0 )
120 ssidd 
 |-  ( ( ph /\ b e. D ) -> ( b supp 0 ) C_ ( b supp 0 ) )
121 0cnd 
 |-  ( ( ph /\ b e. D ) -> 0 e. CC )
122 44 120 49 121 suppssr 
 |-  ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) -> ( b ` i ) = 0 )
123 122 oveq1d 
 |-  ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) -> ( ( b ` i ) .^ ( m ` i ) ) = ( 0 .^ ( m ` i ) ) )
124 123 adantr 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) /\ m e. ( K ^m I ) ) -> ( ( b ` i ) .^ ( m ` i ) ) = ( 0 .^ ( m ` i ) ) )
125 eldifi 
 |-  ( i e. ( I \ ( b supp 0 ) ) -> i e. I )
126 125 111 sylan2 
 |-  ( ( m e. ( K ^m I ) /\ i e. ( I \ ( b supp 0 ) ) ) -> ( m ` i ) e. K )
127 126 ancoms 
 |-  ( ( i e. ( I \ ( b supp 0 ) ) /\ m e. ( K ^m I ) ) -> ( m ` i ) e. K )
128 127 adantll 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) /\ m e. ( K ^m I ) ) -> ( m ` i ) e. K )
129 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
130 7 129 ringidval 
 |-  ( 1r ` S ) = ( 0g ` M )
131 105 130 8 mulg0 
 |-  ( ( m ` i ) e. K -> ( 0 .^ ( m ` i ) ) = ( 1r ` S ) )
132 128 131 syl 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) /\ m e. ( K ^m I ) ) -> ( 0 .^ ( m ` i ) ) = ( 1r ` S ) )
133 124 132 eqtrd 
 |-  ( ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) /\ m e. ( K ^m I ) ) -> ( ( b ` i ) .^ ( m ` i ) ) = ( 1r ` S ) )
134 133 mpteq2dva 
 |-  ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) -> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) = ( m e. ( K ^m I ) |-> ( 1r ` S ) ) )
135 fconstmpt 
 |-  ( ( K ^m I ) X. { ( 1r ` S ) } ) = ( m e. ( K ^m I ) |-> ( 1r ` S ) )
136 22 129 pws1 
 |-  ( ( S e. Ring /\ ( K ^m I ) e. _V ) -> ( ( K ^m I ) X. { ( 1r ` S ) } ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
137 67 68 136 syl2anc 
 |-  ( ph -> ( ( K ^m I ) X. { ( 1r ` S ) } ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
138 137 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) -> ( ( K ^m I ) X. { ( 1r ` S ) } ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
139 135 138 eqtr3id 
 |-  ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) -> ( m e. ( K ^m I ) |-> ( 1r ` S ) ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
140 134 139 eqtrd 
 |-  ( ( ( ph /\ b e. D ) /\ i e. ( I \ ( b supp 0 ) ) ) -> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) = ( 1r ` ( S ^s ( K ^m I ) ) ) )
141 140 49 suppss2 
 |-  ( ( ph /\ b e. D ) -> ( ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) supp ( 1r ` ( S ^s ( K ^m I ) ) ) ) C_ ( b supp 0 ) )
142 114 115 117 119 141 fsuppsssuppgd 
 |-  ( ( ph /\ b e. D ) -> ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) finSupp ( 1r ` ( S ^s ( K ^m I ) ) ) )
143 22 6 102 23 7 103 49 104 113 142 pwsgprod 
 |-  ( ( ph /\ b e. D ) -> ( ( mulGrp ` ( S ^s ( K ^m I ) ) ) gsum ( i e. I |-> ( m e. ( K ^m I ) |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) = ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) )
144 101 143 eqtrd 
 |-  ( ( 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 ) ) ) ) ) = ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) )
145 42 144 oveq12d 
 |-  ( ( 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 ) ) ) ) ) ) = ( ( ( K ^m I ) X. { ( F ` b ) } ) ( .r ` ( S ^s ( K ^m I ) ) ) ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) ) )
146 6 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ K )
147 33 146 eqsstrrd 
 |-  ( R e. ( SubRing ` S ) -> ( Base ` U ) C_ K )
148 12 147 syl 
 |-  ( ph -> ( Base ` U ) C_ K )
149 32 148 fssd 
 |-  ( ph -> F : D --> K )
150 149 ffvelcdmda 
 |-  ( ( ph /\ b e. D ) -> ( F ` b ) e. K )
151 fconst6g 
 |-  ( ( F ` b ) e. K -> ( ( K ^m I ) X. { ( F ` b ) } ) : ( K ^m I ) --> K )
152 150 151 syl 
 |-  ( ( ph /\ b e. D ) -> ( ( K ^m I ) X. { ( F ` b ) } ) : ( K ^m I ) --> K )
153 22 6 55 104 103 152 pwselbasr 
 |-  ( ( ph /\ b e. D ) -> ( ( K ^m I ) X. { ( F ` b ) } ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
154 10 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ m e. ( K ^m I ) ) -> I e. V )
155 11 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ m e. ( K ^m I ) ) -> S e. CRing )
156 simpr 
 |-  ( ( ( ph /\ b e. D ) /\ m e. ( K ^m I ) ) -> m e. ( K ^m I ) )
157 simplr 
 |-  ( ( ( ph /\ b e. D ) /\ m e. ( K ^m I ) ) -> b e. D )
158 5 6 7 8 154 155 156 157 evlsvvvallem 
 |-  ( ( ( ph /\ b e. D ) /\ m e. ( K ^m I ) ) -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) e. K )
159 158 fmpttd 
 |-  ( ( ph /\ b e. D ) -> ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) : ( K ^m I ) --> K )
160 22 6 55 104 103 159 pwselbasr 
 |-  ( ( ph /\ b e. D ) -> ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
161 22 55 104 103 153 160 9 25 pwsmulrval 
 |-  ( ( ph /\ b e. D ) -> ( ( ( K ^m I ) X. { ( F ` b ) } ) ( .r ` ( S ^s ( K ^m I ) ) ) ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) ) = ( ( ( K ^m I ) X. { ( F ` b ) } ) oF .x. ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) ) )
162 152 ffnd 
 |-  ( ( ph /\ b e. D ) -> ( ( K ^m I ) X. { ( F ` b ) } ) Fn ( K ^m I ) )
163 ovex 
 |-  ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) e. _V
164 eqid 
 |-  ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) = ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) )
165 163 164 fnmpti 
 |-  ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) Fn ( K ^m I )
166 165 a1i 
 |-  ( ( ph /\ b e. D ) -> ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) Fn ( K ^m I ) )
167 inidm 
 |-  ( ( K ^m I ) i^i ( K ^m I ) ) = ( K ^m I )
168 fvex 
 |-  ( F ` b ) e. _V
169 168 fvconst2 
 |-  ( l e. ( K ^m I ) -> ( ( ( K ^m I ) X. { ( F ` b ) } ) ` l ) = ( F ` b ) )
170 169 adantl 
 |-  ( ( ( ph /\ b e. D ) /\ l e. ( K ^m I ) ) -> ( ( ( K ^m I ) X. { ( F ` b ) } ) ` l ) = ( F ` b ) )
171 fveq1 
 |-  ( m = l -> ( m ` i ) = ( l ` i ) )
172 171 oveq2d 
 |-  ( m = l -> ( ( b ` i ) .^ ( m ` i ) ) = ( ( b ` i ) .^ ( l ` i ) ) )
173 172 mpteq2dv 
 |-  ( m = l -> ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) = ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) )
174 173 oveq2d 
 |-  ( m = l -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) = ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) )
175 simpr 
 |-  ( ( ( ph /\ b e. D ) /\ l e. ( K ^m I ) ) -> l e. ( K ^m I ) )
176 10 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ l e. ( K ^m I ) ) -> I e. V )
177 11 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ l e. ( K ^m I ) ) -> S e. CRing )
178 simplr 
 |-  ( ( ( ph /\ b e. D ) /\ l e. ( K ^m I ) ) -> b e. D )
179 5 6 7 8 176 177 175 178 evlsvvvallem 
 |-  ( ( ( ph /\ b e. D ) /\ l e. ( K ^m I ) ) -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) e. K )
180 164 174 175 179 fvmptd3 
 |-  ( ( ( ph /\ b e. D ) /\ l e. ( K ^m I ) ) -> ( ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) ` l ) = ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) )
181 162 166 103 103 167 170 180 offval 
 |-  ( ( ph /\ b e. D ) -> ( ( ( K ^m I ) X. { ( F ` b ) } ) oF .x. ( m e. ( K ^m I ) |-> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( m ` i ) ) ) ) ) ) = ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) )
182 145 161 181 3eqtrd 
 |-  ( ( 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 ) ) ) ) ) ) = ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) )
183 182 mpteq2dva 
 |-  ( 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 e. D |-> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) )
184 183 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 ) ) ) ) ) ) ) ) = ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) ) )
185 eqid 
 |-  ( 0g ` ( S ^s ( K ^m I ) ) ) = ( 0g ` ( S ^s ( K ^m I ) ) )
186 ovexd 
 |-  ( ph -> ( NN0 ^m I ) e. _V )
187 5 186 rabexd 
 |-  ( ph -> D e. _V )
188 67 ringcmnd 
 |-  ( ph -> S e. CMnd )
189 67 adantr 
 |-  ( ( ph /\ ( l e. ( K ^m I ) /\ b e. D ) ) -> S e. Ring )
190 150 adantrl 
 |-  ( ( ph /\ ( l e. ( K ^m I ) /\ b e. D ) ) -> ( F ` b ) e. K )
191 simpl 
 |-  ( ( ph /\ ( l e. ( K ^m I ) /\ b e. D ) ) -> ph )
192 simprr 
 |-  ( ( ph /\ ( l e. ( K ^m I ) /\ b e. D ) ) -> b e. D )
193 simprl 
 |-  ( ( ph /\ ( l e. ( K ^m I ) /\ b e. D ) ) -> l e. ( K ^m I ) )
194 191 192 193 179 syl21anc 
 |-  ( ( ph /\ ( l e. ( K ^m I ) /\ b e. D ) ) -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) e. K )
195 6 9 189 190 194 ringcld 
 |-  ( ( ph /\ ( l e. ( K ^m I ) /\ b e. D ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) e. K )
196 187 mptexd 
 |-  ( ph -> ( b e. D |-> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) e. _V )
197 fvexd 
 |-  ( ph -> ( 0g ` ( S ^s ( K ^m I ) ) ) e. _V )
198 funmpt 
 |-  Fun ( b e. D |-> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) )
199 198 a1i 
 |-  ( ph -> Fun ( b e. D |-> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) )
200 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
201 4 ovexi 
 |-  U e. _V
202 201 a1i 
 |-  ( ph -> U e. _V )
203 2 3 200 13 202 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` U ) )
204 ssidd 
 |-  ( ph -> ( F supp ( 0g ` U ) ) C_ ( F supp ( 0g ` U ) ) )
205 fvexd 
 |-  ( ph -> ( 0g ` U ) e. _V )
206 149 204 187 205 suppssr 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( F ` b ) = ( 0g ` U ) )
207 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
208 4 207 subrg0 
 |-  ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
209 12 208 syl 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` U ) )
210 209 adantr 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( 0g ` S ) = ( 0g ` U ) )
211 206 210 eqtr4d 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( F ` b ) = ( 0g ` S ) )
212 211 adantr 
 |-  ( ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) /\ l e. ( K ^m I ) ) -> ( F ` b ) = ( 0g ` S ) )
213 212 oveq1d 
 |-  ( ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) /\ l e. ( K ^m I ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) = ( ( 0g ` S ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) )
214 67 ad2antrr 
 |-  ( ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) /\ l e. ( K ^m I ) ) -> S e. Ring )
215 eldifi 
 |-  ( b e. ( D \ ( F supp ( 0g ` U ) ) ) -> b e. D )
216 215 179 sylanl2 
 |-  ( ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) /\ l e. ( K ^m I ) ) -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) e. K )
217 6 9 207 214 216 ringlzd 
 |-  ( ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) /\ l e. ( K ^m I ) ) -> ( ( 0g ` S ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) = ( 0g ` S ) )
218 213 217 eqtrd 
 |-  ( ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) /\ l e. ( K ^m I ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) = ( 0g ` S ) )
219 218 mpteq2dva 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) = ( l e. ( K ^m I ) |-> ( 0g ` S ) ) )
220 fconstmpt 
 |-  ( ( K ^m I ) X. { ( 0g ` S ) } ) = ( l e. ( K ^m I ) |-> ( 0g ` S ) )
221 188 cmnmndd 
 |-  ( ph -> S e. Mnd )
222 22 207 pws0g 
 |-  ( ( S e. Mnd /\ ( K ^m I ) e. _V ) -> ( ( K ^m I ) X. { ( 0g ` S ) } ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
223 221 68 222 syl2anc 
 |-  ( ph -> ( ( K ^m I ) X. { ( 0g ` S ) } ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
224 220 223 eqtr3id 
 |-  ( ph -> ( l e. ( K ^m I ) |-> ( 0g ` S ) ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
225 224 adantr 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( l e. ( K ^m I ) |-> ( 0g ` S ) ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
226 219 225 eqtrd 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) = ( 0g ` ( S ^s ( K ^m I ) ) ) )
227 226 187 suppss2 
 |-  ( ph -> ( ( b e. D |-> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) supp ( 0g ` ( S ^s ( K ^m I ) ) ) ) C_ ( F supp ( 0g ` U ) ) )
228 196 197 199 203 227 fsuppsssuppgd 
 |-  ( ph -> ( b e. D |-> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) finSupp ( 0g ` ( S ^s ( K ^m I ) ) ) )
229 22 6 185 68 187 188 195 228 pwsgsum 
 |-  ( ph -> ( ( S ^s ( K ^m I ) ) gsum ( b e. D |-> ( l e. ( K ^m I ) |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) ) = ( l e. ( K ^m I ) |-> ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) ) )
230 28 184 229 3eqtrd 
 |-  ( ph -> ( Q ` F ) = ( l e. ( K ^m I ) |-> ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( l ` i ) ) ) ) ) ) ) ) )
231 ovexd 
 |-  ( ph -> ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) e. _V )
232 21 230 14 231 fvmptd4 
 |-  ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )