This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid 
 |-  ( 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 8 4 mgpbas 
 |-  B = ( Base ` G )
32 3 ply1ring 
 |-  ( R e. Ring -> W e. Ring )
33 20 32 syl 
 |-  ( ph -> W e. Ring )
34 8 ringmgp 
 |-  ( W e. Ring -> G e. Mnd )
35 33 34 syl 
 |-  ( ph -> G e. Mnd )
36 35 adantr 
 |-  ( ( ph /\ x e. M ) -> G e. Mnd )
37 16 r19.21bi 
 |-  ( ( ph /\ x e. M ) -> N e. NN0 )
38 20 adantr 
 |-  ( ( ph /\ x e. M ) -> R e. Ring )
39 5 3 4 vr1cl 
 |-  ( R e. Ring -> X e. B )
40 38 39 syl 
 |-  ( ( ph /\ x e. M ) -> X e. B )
41 31 9 36 37 40 mulgnn0cld 
 |-  ( ( ph /\ x e. M ) -> ( N .^ X ) e. B )
42 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
43 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
44 4 42 10 43 lmodvscl 
 |-  ( ( W e. LMod /\ A e. ( Base ` ( Scalar ` W ) ) /\ ( N .^ X ) e. B ) -> ( A .X. ( N .^ X ) ) e. B )
45 23 30 41 44 syl3anc 
 |-  ( ( ph /\ x e. M ) -> ( A .X. ( N .^ X ) ) e. B )
46 1 2 3 18 4 12 45 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 ) ) ) )
47 12 adantr 
 |-  ( ( ph /\ x e. M ) -> R e. CRing )
48 17 adantr 
 |-  ( ( ph /\ x e. M ) -> C e. K )
49 1 3 8 5 2 9 47 37 10 24 48 6 7 11 evl1scvarpwval 
 |-  ( ( ph /\ x e. M ) -> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) = ( A .x. ( N E C ) ) )
50 49 mpteq2dva 
 |-  ( ph -> ( x e. M |-> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) ) = ( x e. M |-> ( A .x. ( N E C ) ) ) )
51 50 oveq2d 
 |-  ( ph -> ( R gsum ( x e. M |-> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) ) ) = ( R gsum ( x e. M |-> ( A .x. ( N E C ) ) ) ) )
52 46 51 eqtrd 
 |-  ( ph -> ( ( Q ` ( W gsum ( x e. M |-> ( A .X. ( N .^ X ) ) ) ) ) ` C ) = ( R gsum ( x e. M |-> ( A .x. ( N E C ) ) ) ) )