Metamath Proof Explorer

Theorem evls1fpws

Description: Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025)

Ref Expression
Hypotheses ressply1evl2.q 
|- Q = ( S evalSub1 R )
ressply1evl2.k 
|- K = ( Base ` S )
ressply1evl2.w 
|- W = ( Poly1 ` U )
ressply1evl2.u 
|- U = ( S |`s R )
ressply1evl2.b 
|- B = ( Base ` W )
evls1fpws.s 
|- ( ph -> S e. CRing )
evls1fpws.r 
|- ( ph -> R e. ( SubRing ` S ) )
evls1fpws.y 
|- ( ph -> M e. B )
evls1fpws.1 
|- .x. = ( .r ` S )
evls1fpws.2 
|- .^ = ( .g ` ( mulGrp ` S ) )
evls1fpws.a 
|- A = ( coe1 ` M )
Assertion evls1fpws 
|- ( ph -> ( Q ` M ) = ( x e. K |-> ( S gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ressply1evl2.q 
 |-  Q = ( S evalSub1 R )
2 ressply1evl2.k 
 |-  K = ( Base ` S )
3 ressply1evl2.w 
 |-  W = ( Poly1 ` U )
4 ressply1evl2.u 
 |-  U = ( S |`s R )
5 ressply1evl2.b 
 |-  B = ( Base ` W )
6 evls1fpws.s 
 |-  ( ph -> S e. CRing )
7 evls1fpws.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
8 evls1fpws.y 
 |-  ( ph -> M e. B )
9 evls1fpws.1 
 |-  .x. = ( .r ` S )
10 evls1fpws.2 
 |-  .^ = ( .g ` ( mulGrp ` S ) )
11 evls1fpws.a 
 |-  A = ( coe1 ` M )
12 4 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
13 7 12 syl 
 |-  ( ph -> U e. Ring )
14 eqid 
 |-  ( var1 ` U ) = ( var1 ` U )
15 eqid 
 |-  ( .s ` W ) = ( .s ` W )
16 eqid 
 |-  ( mulGrp ` W ) = ( mulGrp ` W )
17 eqid 
 |-  ( .g ` ( mulGrp ` W ) ) = ( .g ` ( mulGrp ` W ) )
18 3 14 5 15 16 17 11 ply1coe 
 |-  ( ( U e. Ring /\ M e. B ) -> M = ( W gsum ( k e. NN0 |-> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) ) )
19 13 8 18 syl2anc 
 |-  ( ph -> M = ( W gsum ( k e. NN0 |-> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) ) )
20 19 fveq2d 
 |-  ( ph -> ( Q ` M ) = ( Q ` ( W gsum ( k e. NN0 |-> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) ) ) )
21 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
22 eqid 
 |-  ( S ^s K ) = ( S ^s K )
23 3 ply1lmod 
 |-  ( U e. Ring -> W e. LMod )
24 13 23 syl 
 |-  ( ph -> W e. LMod )
25 24 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> W e. LMod )
26 eqid 
 |-  ( Base ` U ) = ( Base ` U )
27 11 5 3 26 coe1fvalcl 
 |-  ( ( M e. B /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` U ) )
28 8 27 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` U ) )
29 3 ply1sca 
 |-  ( U e. Ring -> U = ( Scalar ` W ) )
30 13 29 syl 
 |-  ( ph -> U = ( Scalar ` W ) )
31 30 fveq2d 
 |-  ( ph -> ( Base ` U ) = ( Base ` ( Scalar ` W ) ) )
32 31 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( Base ` U ) = ( Base ` ( Scalar ` W ) ) )
33 28 32 eleqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` ( Scalar ` W ) ) )
34 16 5 mgpbas 
 |-  B = ( Base ` ( mulGrp ` W ) )
35 3 ply1ring 
 |-  ( U e. Ring -> W e. Ring )
36 13 35 syl 
 |-  ( ph -> W e. Ring )
37 36 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> W e. Ring )
38 16 ringmgp 
 |-  ( W e. Ring -> ( mulGrp ` W ) e. Mnd )
39 37 38 syl 
 |-  ( ( ph /\ k e. NN0 ) -> ( mulGrp ` W ) e. Mnd )
40 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
41 13 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> U e. Ring )
42 14 3 5 vr1cl 
 |-  ( U e. Ring -> ( var1 ` U ) e. B )
43 41 42 syl 
 |-  ( ( ph /\ k e. NN0 ) -> ( var1 ` U ) e. B )
44 34 17 39 40 43 mulgnn0cld 
 |-  ( ( ph /\ k e. NN0 ) -> ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) e. B )
45 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
46 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
47 5 45 15 46 lmodvscl 
 |-  ( ( W e. LMod /\ ( A ` k ) e. ( Base ` ( Scalar ` W ) ) /\ ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) e. B ) -> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) e. B )
48 25 33 44 47 syl3anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) e. B )
49 ssidd 
 |-  ( ph -> NN0 C_ NN0 )
50 fvexd 
 |-  ( ph -> ( 0g ` W ) e. _V )
51 fveq2 
 |-  ( k = j -> ( A ` k ) = ( A ` j ) )
52 oveq1 
 |-  ( k = j -> ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) = ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) )
53 51 52 oveq12d 
 |-  ( k = j -> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( ( A ` j ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) )
54 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
55 11 5 3 54 coe1ae0 
 |-  ( M e. B -> E. i e. NN0 A. j e. NN0 ( i < j -> ( A ` j ) = ( 0g ` U ) ) )
56 8 55 syl 
 |-  ( ph -> E. i e. NN0 A. j e. NN0 ( i < j -> ( A ` j ) = ( 0g ` U ) ) )
57 simpr 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> ( A ` j ) = ( 0g ` U ) )
58 30 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> U = ( Scalar ` W ) )
59 58 fveq2d 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> ( 0g ` U ) = ( 0g ` ( Scalar ` W ) ) )
60 57 59 eqtrd 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> ( A ` j ) = ( 0g ` ( Scalar ` W ) ) )
61 60 oveq1d 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> ( ( A ` j ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) )
62 24 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> W e. LMod )
63 36 38 syl 
 |-  ( ph -> ( mulGrp ` W ) e. Mnd )
64 63 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( mulGrp ` W ) e. Mnd )
65 simpr 
 |-  ( ( ph /\ j e. NN0 ) -> j e. NN0 )
66 13 42 syl 
 |-  ( ph -> ( var1 ` U ) e. B )
67 66 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( var1 ` U ) e. B )
68 34 17 64 65 67 mulgnn0cld 
 |-  ( ( ph /\ j e. NN0 ) -> ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) e. B )
69 68 ad4ant13 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) e. B )
70 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
71 5 45 15 70 21 lmod0vs 
 |-  ( ( W e. LMod /\ ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) e. B ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( 0g ` W ) )
72 62 69 71 syl2anc 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( 0g ` W ) )
73 61 72 eqtrd 
 |-  ( ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) /\ ( A ` j ) = ( 0g ` U ) ) -> ( ( A ` j ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( 0g ` W ) )
74 73 ex 
 |-  ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) -> ( ( A ` j ) = ( 0g ` U ) -> ( ( A ` j ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( 0g ` W ) ) )
75 74 imim2d 
 |-  ( ( ( ph /\ i e. NN0 ) /\ j e. NN0 ) -> ( ( i < j -> ( A ` j ) = ( 0g ` U ) ) -> ( i < j -> ( ( A ` j ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( 0g ` W ) ) ) )
76 75 ralimdva 
 |-  ( ( ph /\ i e. NN0 ) -> ( A. j e. NN0 ( i < j -> ( A ` j ) = ( 0g ` U ) ) -> A. j e. NN0 ( i < j -> ( ( A ` j ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( 0g ` W ) ) ) )
77 76 reximdva 
 |-  ( ph -> ( E. i e. NN0 A. j e. NN0 ( i < j -> ( A ` j ) = ( 0g ` U ) ) -> E. i e. NN0 A. j e. NN0 ( i < j -> ( ( A ` j ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( 0g ` W ) ) ) )
78 56 77 mpd 
 |-  ( ph -> E. i e. NN0 A. j e. NN0 ( i < j -> ( ( A ` j ) ( .s ` W ) ( j ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( 0g ` W ) ) )
79 50 48 53 78 mptnn0fsuppd 
 |-  ( ph -> ( k e. NN0 |-> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) finSupp ( 0g ` W ) )
80 1 2 3 21 4 22 5 6 7 48 49 79 evls1gsumadd 
 |-  ( ph -> ( Q ` ( W gsum ( k e. NN0 |-> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) ) ) = ( ( S ^s K ) gsum ( k e. NN0 |-> ( Q ` ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) ) ) )
81 1 2 22 4 3 evls1rhm 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom ( S ^s K ) ) )
82 6 7 81 syl2anc 
 |-  ( ph -> Q e. ( W RingHom ( S ^s K ) ) )
83 82 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> Q e. ( W RingHom ( S ^s K ) ) )
84 eqid 
 |-  ( algSc ` W ) = ( algSc ` W )
85 84 45 36 24 46 5 asclf 
 |-  ( ph -> ( algSc ` W ) : ( Base ` ( Scalar ` W ) ) --> B )
86 85 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( algSc ` W ) : ( Base ` ( Scalar ` W ) ) --> B )
87 86 33 ffvelcdmd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( algSc ` W ) ` ( A ` k ) ) e. B )
88 eqid 
 |-  ( .r ` W ) = ( .r ` W )
89 eqid 
 |-  ( .r ` ( S ^s K ) ) = ( .r ` ( S ^s K ) )
90 5 88 89 rhmmul 
 |-  ( ( Q e. ( W RingHom ( S ^s K ) ) /\ ( ( algSc ` W ) ` ( A ` k ) ) e. B /\ ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) e. B ) -> ( Q ` ( ( ( algSc ` W ) ` ( A ` k ) ) ( .r ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) = ( ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) ( .r ` ( S ^s K ) ) ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) )
91 83 87 44 90 syl3anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( ( ( algSc ` W ) ` ( A ` k ) ) ( .r ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) = ( ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) ( .r ` ( S ^s K ) ) ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) )
92 4 subrgcrng 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> U e. CRing )
93 6 7 92 syl2anc 
 |-  ( ph -> U e. CRing )
94 3 ply1assa 
 |-  ( U e. CRing -> W e. AssAlg )
95 93 94 syl 
 |-  ( ph -> W e. AssAlg )
96 95 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> W e. AssAlg )
97 84 45 46 5 88 15 asclmul1 
 |-  ( ( W e. AssAlg /\ ( A ` k ) e. ( Base ` ( Scalar ` W ) ) /\ ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) e. B ) -> ( ( ( algSc ` W ) ` ( A ` k ) ) ( .r ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) )
98 96 33 44 97 syl3anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( algSc ` W ) ` ( A ` k ) ) ( .r ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) = ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) )
99 98 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( ( ( algSc ` W ) ` ( A ` k ) ) ( .r ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) = ( Q ` ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) )
100 eqid 
 |-  ( Base ` ( S ^s K ) ) = ( Base ` ( S ^s K ) )
101 6 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> S e. CRing )
102 2 fvexi 
 |-  K e. _V
103 102 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> K e. _V )
104 5 100 rhmf 
 |-  ( Q e. ( W RingHom ( S ^s K ) ) -> Q : B --> ( Base ` ( S ^s K ) ) )
105 83 104 syl 
 |-  ( ( ph /\ k e. NN0 ) -> Q : B --> ( Base ` ( S ^s K ) ) )
106 105 87 ffvelcdmd 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) e. ( Base ` ( S ^s K ) ) )
107 105 44 ffvelcdmd 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) e. ( Base ` ( S ^s K ) ) )
108 22 100 101 103 106 107 9 89 pwsmulrval 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) ( .r ` ( S ^s K ) ) ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) = ( ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) oF .x. ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) )
109 22 2 100 101 103 106 pwselbas 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) : K --> K )
110 109 ffnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) Fn K )
111 22 2 100 101 103 107 pwselbas 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) : K --> K )
112 111 ffnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) Fn K )
113 inidm 
 |-  ( K i^i K ) = K
114 6 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> S e. CRing )
115 7 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> R e. ( SubRing ` S ) )
116 2 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ K )
117 7 116 syl 
 |-  ( ph -> R C_ K )
118 4 2 ressbas2 
 |-  ( R C_ K -> R = ( Base ` U ) )
119 117 118 syl 
 |-  ( ph -> R = ( Base ` U ) )
120 119 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> R = ( Base ` U ) )
121 28 120 eleqtrrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. R )
122 121 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> ( A ` k ) e. R )
123 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> x e. K )
124 1 3 4 2 84 114 115 122 123 evls1scafv 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> ( ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) ` x ) = ( A ` k ) )
125 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> k e. NN0 )
126 1 4 3 14 2 17 10 114 115 125 123 evls1varpwval 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> ( ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ` x ) = ( k .^ x ) )
127 110 112 103 103 113 124 126 offval 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) oF .x. ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) = ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) )
128 108 127 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( Q ` ( ( algSc ` W ) ` ( A ` k ) ) ) ( .r ` ( S ^s K ) ) ( Q ` ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) = ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) )
129 91 99 128 3eqtr3d 
 |-  ( ( ph /\ k e. NN0 ) -> ( Q ` ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) = ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) )
130 129 mpteq2dva 
 |-  ( ph -> ( k e. NN0 |-> ( Q ` ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) ) = ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) )
131 130 oveq2d 
 |-  ( ph -> ( ( S ^s K ) gsum ( k e. NN0 |-> ( Q ` ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) ) ) = ( ( S ^s K ) gsum ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) ) )
132 eqid 
 |-  ( 0g ` ( S ^s K ) ) = ( 0g ` ( S ^s K ) )
133 102 a1i 
 |-  ( ph -> K e. _V )
134 nn0ex 
 |-  NN0 e. _V
135 134 a1i 
 |-  ( ph -> NN0 e. _V )
136 6 crngringd 
 |-  ( ph -> S e. Ring )
137 136 ringcmnd 
 |-  ( ph -> S e. CMnd )
138 136 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> S e. Ring )
139 7 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> R e. ( SubRing ` S ) )
140 139 116 syl 
 |-  ( ( ph /\ k e. NN0 ) -> R C_ K )
141 140 121 sseldd 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. K )
142 141 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> ( A ` k ) e. K )
143 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
144 143 2 mgpbas 
 |-  K = ( Base ` ( mulGrp ` S ) )
145 143 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
146 136 145 syl 
 |-  ( ph -> ( mulGrp ` S ) e. Mnd )
147 146 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> ( mulGrp ` S ) e. Mnd )
148 144 10 147 125 123 mulgnn0cld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> ( k .^ x ) e. K )
149 2 9 138 142 148 ringcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ x e. K ) -> ( ( A ` k ) .x. ( k .^ x ) ) e. K )
150 149 3impa 
 |-  ( ( ph /\ k e. NN0 /\ x e. K ) -> ( ( A ` k ) .x. ( k .^ x ) ) e. K )
151 150 3com23 
 |-  ( ( ph /\ x e. K /\ k e. NN0 ) -> ( ( A ` k ) .x. ( k .^ x ) ) e. K )
152 151 3expb 
 |-  ( ( ph /\ ( x e. K /\ k e. NN0 ) ) -> ( ( A ` k ) .x. ( k .^ x ) ) e. K )
153 135 mptexd 
 |-  ( ph -> ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) e. _V )
154 funmpt 
 |-  Fun ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) )
155 154 a1i 
 |-  ( ph -> Fun ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) )
156 fvexd 
 |-  ( ph -> ( 0g ` ( S ^s K ) ) e. _V )
157 11 5 3 54 coe1sfi 
 |-  ( M e. B -> A finSupp ( 0g ` U ) )
158 8 157 syl 
 |-  ( ph -> A finSupp ( 0g ` U ) )
159 158 fsuppimpd 
 |-  ( ph -> ( A supp ( 0g ` U ) ) e. Fin )
160 11 5 3 26 coe1f 
 |-  ( M e. B -> A : NN0 --> ( Base ` U ) )
161 8 160 syl 
 |-  ( ph -> A : NN0 --> ( Base ` U ) )
162 161 ffnd 
 |-  ( ph -> A Fn NN0 )
163 162 adantr 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> A Fn NN0 )
164 134 a1i 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> NN0 e. _V )
165 fvexd 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> ( 0g ` U ) e. _V )
166 simpr 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) )
167 163 164 165 166 fvdifsupp 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> ( A ` k ) = ( 0g ` U ) )
168 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
169 4 168 subrg0 
 |-  ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
170 7 169 syl 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` U ) )
171 170 adantr 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> ( 0g ` S ) = ( 0g ` U ) )
172 167 171 eqtr4d 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> ( A ` k ) = ( 0g ` S ) )
173 172 adantr 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> ( A ` k ) = ( 0g ` S ) )
174 173 oveq1d 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> ( ( A ` k ) .x. ( k .^ x ) ) = ( ( 0g ` S ) .x. ( k .^ x ) ) )
175 136 ad2antrr 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> S e. Ring )
176 175 145 syl 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> ( mulGrp ` S ) e. Mnd )
177 simplr 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) )
178 177 eldifad 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> k e. NN0 )
179 simpr 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> x e. K )
180 144 10 176 178 179 mulgnn0cld 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> ( k .^ x ) e. K )
181 2 9 168 ringlz 
 |-  ( ( S e. Ring /\ ( k .^ x ) e. K ) -> ( ( 0g ` S ) .x. ( k .^ x ) ) = ( 0g ` S ) )
182 175 180 181 syl2anc 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> ( ( 0g ` S ) .x. ( k .^ x ) ) = ( 0g ` S ) )
183 174 182 eqtrd 
 |-  ( ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) /\ x e. K ) -> ( ( A ` k ) .x. ( k .^ x ) ) = ( 0g ` S ) )
184 183 mpteq2dva 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) = ( x e. K |-> ( 0g ` S ) ) )
185 fconstmpt 
 |-  ( K X. { ( 0g ` S ) } ) = ( x e. K |-> ( 0g ` S ) )
186 184 185 eqtr4di 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) = ( K X. { ( 0g ` S ) } ) )
187 137 cmnmndd 
 |-  ( ph -> S e. Mnd )
188 22 168 pws0g 
 |-  ( ( S e. Mnd /\ K e. _V ) -> ( K X. { ( 0g ` S ) } ) = ( 0g ` ( S ^s K ) ) )
189 187 133 188 syl2anc 
 |-  ( ph -> ( K X. { ( 0g ` S ) } ) = ( 0g ` ( S ^s K ) ) )
190 189 adantr 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> ( K X. { ( 0g ` S ) } ) = ( 0g ` ( S ^s K ) ) )
191 186 190 eqtrd 
 |-  ( ( ph /\ k e. ( NN0 \ ( A supp ( 0g ` U ) ) ) ) -> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) = ( 0g ` ( S ^s K ) ) )
192 191 135 suppss2 
 |-  ( ph -> ( ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) supp ( 0g ` ( S ^s K ) ) ) C_ ( A supp ( 0g ` U ) ) )
193 suppssfifsupp 
 |-  ( ( ( ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) /\ ( 0g ` ( S ^s K ) ) e. _V ) /\ ( ( A supp ( 0g ` U ) ) e. Fin /\ ( ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) supp ( 0g ` ( S ^s K ) ) ) C_ ( A supp ( 0g ` U ) ) ) ) -> ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) finSupp ( 0g ` ( S ^s K ) ) )
194 153 155 156 159 192 193 syl32anc 
 |-  ( ph -> ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) finSupp ( 0g ` ( S ^s K ) ) )
195 22 2 132 133 135 137 152 194 pwsgsum 
 |-  ( ph -> ( ( S ^s K ) gsum ( k e. NN0 |-> ( x e. K |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) ) = ( x e. K |-> ( S gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) ) )
196 80 131 195 3eqtrd 
 |-  ( ph -> ( Q ` ( W gsum ( k e. NN0 |-> ( ( A ` k ) ( .s ` W ) ( k ( .g ` ( mulGrp ` W ) ) ( var1 ` U ) ) ) ) ) ) = ( x e. K |-> ( S gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) ) )
197 20 196 eqtrd 
 |-  ( ph -> ( Q ` M ) = ( x e. K |-> ( S gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) ) )