Metamath Proof Explorer


Theorem evl1gsummon

Description: Value of a univariate polynomial evaluation mapping an additive group sum of a multiple of an exponentiation of a variable to a group sum of the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019)

Ref Expression
Hypotheses evl1gsummon.q
|- Q = ( eval1 ` R )
evl1gsummon.k
|- K = ( Base ` R )
evl1gsummon.w
|- W = ( Poly1 ` R )
evl1gsummon.b
|- B = ( Base ` W )
evl1gsummon.x
|- X = ( var1 ` R )
evl1gsummon.h
|- H = ( mulGrp ` R )
evl1gsummon.e
|- E = ( .g ` H )
evl1gsummon.g
|- G = ( mulGrp ` W )
evl1gsummon.p
|- .^ = ( .g ` G )
evl1gsummon.t1
|- .X. = ( .s ` W )
evl1gsummon.t2
|- .x. = ( .r ` R )
evl1gsummon.r
|- ( ph -> R e. CRing )
evl1gsummon.a
|- ( ph -> A. x e. M A e. K )
evl1gsummon.m
|- ( ph -> M C_ NN0 )
evl1gsummon.f
|- ( ph -> M e. Fin )
evl1gsummon.n
|- ( ph -> A. x e. M N e. NN0 )
evl1gsummon.c
|- ( ph -> C e. K )
Assertion evl1gsummon
|- ( ph -> ( ( Q ` ( W gsum ( x e. M |-> ( A .X. ( N .^ X ) ) ) ) ) ` C ) = ( R gsum ( x e. M |-> ( A .x. ( N E C ) ) ) ) )

Proof

Step Hyp Ref Expression
1 evl1gsummon.q
 |-  Q = ( eval1 ` R )
2 evl1gsummon.k
 |-  K = ( Base ` R )
3 evl1gsummon.w
 |-  W = ( Poly1 ` R )
4 evl1gsummon.b
 |-  B = ( Base ` W )
5 evl1gsummon.x
 |-  X = ( var1 ` R )
6 evl1gsummon.h
 |-  H = ( mulGrp ` R )
7 evl1gsummon.e
 |-  E = ( .g ` H )
8 evl1gsummon.g
 |-  G = ( mulGrp ` W )
9 evl1gsummon.p
 |-  .^ = ( .g ` G )
10 evl1gsummon.t1
 |-  .X. = ( .s ` W )
11 evl1gsummon.t2
 |-  .x. = ( .r ` R )
12 evl1gsummon.r
 |-  ( ph -> R e. CRing )
13 evl1gsummon.a
 |-  ( ph -> A. x e. M A e. K )
14 evl1gsummon.m
 |-  ( ph -> M C_ NN0 )
15 evl1gsummon.f
 |-  ( ph -> M e. Fin )
16 evl1gsummon.n
 |-  ( ph -> A. x e. M N e. NN0 )
17 evl1gsummon.c
 |-  ( ph -> C e. K )
18 eqid
 |-  ( R ^s K ) = ( R ^s K )
19 crngring
 |-  ( R e. CRing -> R e. Ring )
20 12 19 syl
 |-  ( ph -> R e. Ring )
21 3 ply1lmod
 |-  ( R e. Ring -> W e. LMod )
22 20 21 syl
 |-  ( ph -> W e. LMod )
23 22 adantr
 |-  ( ( ph /\ x e. M ) -> W e. LMod )
24 13 r19.21bi
 |-  ( ( ph /\ x e. M ) -> A e. K )
25 3 ply1sca
 |-  ( R e. CRing -> R = ( Scalar ` W ) )
26 12 25 syl
 |-  ( ph -> R = ( Scalar ` W ) )
27 26 fveq2d
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` W ) ) )
28 2 27 syl5eq
 |-  ( ph -> K = ( Base ` ( Scalar ` W ) ) )
29 28 adantr
 |-  ( ( ph /\ x e. M ) -> K = ( Base ` ( Scalar ` W ) ) )
30 24 29 eleqtrd
 |-  ( ( ph /\ x e. M ) -> A e. ( Base ` ( Scalar ` W ) ) )
31 3 ply1ring
 |-  ( R e. Ring -> W e. Ring )
32 20 31 syl
 |-  ( ph -> W e. Ring )
33 8 ringmgp
 |-  ( W e. Ring -> G e. Mnd )
34 32 33 syl
 |-  ( ph -> G e. Mnd )
35 34 adantr
 |-  ( ( ph /\ x e. M ) -> G e. Mnd )
36 16 r19.21bi
 |-  ( ( ph /\ x e. M ) -> N e. NN0 )
37 20 adantr
 |-  ( ( ph /\ x e. M ) -> R e. Ring )
38 5 3 4 vr1cl
 |-  ( R e. Ring -> X e. B )
39 37 38 syl
 |-  ( ( ph /\ x e. M ) -> X e. B )
40 8 4 mgpbas
 |-  B = ( Base ` G )
41 40 9 mulgnn0cl
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .^ X ) e. B )
42 35 36 39 41 syl3anc
 |-  ( ( ph /\ x e. M ) -> ( N .^ X ) e. B )
43 eqid
 |-  ( Scalar ` W ) = ( Scalar ` W )
44 eqid
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
45 4 43 10 44 lmodvscl
 |-  ( ( W e. LMod /\ A e. ( Base ` ( Scalar ` W ) ) /\ ( N .^ X ) e. B ) -> ( A .X. ( N .^ X ) ) e. B )
46 23 30 42 45 syl3anc
 |-  ( ( ph /\ x e. M ) -> ( A .X. ( N .^ X ) ) e. B )
47 1 2 3 18 4 12 46 14 15 17 evl1gsumaddval
 |-  ( ph -> ( ( Q ` ( W gsum ( x e. M |-> ( A .X. ( N .^ X ) ) ) ) ) ` C ) = ( R gsum ( x e. M |-> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) ) ) )
48 12 adantr
 |-  ( ( ph /\ x e. M ) -> R e. CRing )
49 17 adantr
 |-  ( ( ph /\ x e. M ) -> C e. K )
50 1 3 8 5 2 9 48 36 10 24 49 6 7 11 evl1scvarpwval
 |-  ( ( ph /\ x e. M ) -> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) = ( A .x. ( N E C ) ) )
51 50 mpteq2dva
 |-  ( ph -> ( x e. M |-> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) ) = ( x e. M |-> ( A .x. ( N E C ) ) ) )
52 51 oveq2d
 |-  ( ph -> ( R gsum ( x e. M |-> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) ) ) = ( R gsum ( x e. M |-> ( A .x. ( N E C ) ) ) ) )
53 47 52 eqtrd
 |-  ( ph -> ( ( Q ` ( W gsum ( x e. M |-> ( A .X. ( N .^ X ) ) ) ) ) ` C ) = ( R gsum ( x e. M |-> ( A .x. ( N E C ) ) ) ) )