Metamath Proof Explorer


Theorem evl1gsumadd

Description: Univariate polynomial evaluation maps (additive) group sums to group sums. Remark: the proof would be shorter if the theorem is proved directly instead of using evls1gsumadd . (Contributed by AV, 15-Sep-2019)

Ref Expression
Hypotheses evl1gsumadd.q
|- Q = ( eval1 ` R )
evl1gsumadd.k
|- K = ( Base ` R )
evl1gsumadd.w
|- W = ( Poly1 ` R )
evl1gsumadd.p
|- P = ( R ^s K )
evl1gsumadd.b
|- B = ( Base ` W )
evl1gsumadd.r
|- ( ph -> R e. CRing )
evl1gsumadd.y
|- ( ( ph /\ x e. N ) -> Y e. B )
evl1gsumadd.n
|- ( ph -> N C_ NN0 )
evl1gsumadd.0
|- .0. = ( 0g ` W )
evl1gsumadd.f
|- ( ph -> ( x e. N |-> Y ) finSupp .0. )
Assertion evl1gsumadd
|- ( ph -> ( Q ` ( W gsum ( x e. N |-> Y ) ) ) = ( P gsum ( x e. N |-> ( Q ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 evl1gsumadd.q
 |-  Q = ( eval1 ` R )
2 evl1gsumadd.k
 |-  K = ( Base ` R )
3 evl1gsumadd.w
 |-  W = ( Poly1 ` R )
4 evl1gsumadd.p
 |-  P = ( R ^s K )
5 evl1gsumadd.b
 |-  B = ( Base ` W )
6 evl1gsumadd.r
 |-  ( ph -> R e. CRing )
7 evl1gsumadd.y
 |-  ( ( ph /\ x e. N ) -> Y e. B )
8 evl1gsumadd.n
 |-  ( ph -> N C_ NN0 )
9 evl1gsumadd.0
 |-  .0. = ( 0g ` W )
10 evl1gsumadd.f
 |-  ( ph -> ( x e. N |-> Y ) finSupp .0. )
11 1 2 evl1fval1
 |-  Q = ( R evalSub1 K )
12 11 a1i
 |-  ( ph -> Q = ( R evalSub1 K ) )
13 12 fveq1d
 |-  ( ph -> ( Q ` ( W gsum ( x e. N |-> Y ) ) ) = ( ( R evalSub1 K ) ` ( W gsum ( x e. N |-> Y ) ) ) )
14 2 ressid
 |-  ( R e. CRing -> ( R |`s K ) = R )
15 6 14 syl
 |-  ( ph -> ( R |`s K ) = R )
16 15 eqcomd
 |-  ( ph -> R = ( R |`s K ) )
17 16 fveq2d
 |-  ( ph -> ( Poly1 ` R ) = ( Poly1 ` ( R |`s K ) ) )
18 3 17 syl5eq
 |-  ( ph -> W = ( Poly1 ` ( R |`s K ) ) )
19 18 fvoveq1d
 |-  ( ph -> ( ( R evalSub1 K ) ` ( W gsum ( x e. N |-> Y ) ) ) = ( ( R evalSub1 K ) ` ( ( Poly1 ` ( R |`s K ) ) gsum ( x e. N |-> Y ) ) ) )
20 eqid
 |-  ( R evalSub1 K ) = ( R evalSub1 K )
21 eqid
 |-  ( Poly1 ` ( R |`s K ) ) = ( Poly1 ` ( R |`s K ) )
22 eqid
 |-  ( 0g ` ( Poly1 ` ( R |`s K ) ) ) = ( 0g ` ( Poly1 ` ( R |`s K ) ) )
23 eqid
 |-  ( R |`s K ) = ( R |`s K )
24 eqid
 |-  ( Base ` ( Poly1 ` ( R |`s K ) ) ) = ( Base ` ( Poly1 ` ( R |`s K ) ) )
25 crngring
 |-  ( R e. CRing -> R e. Ring )
26 2 subrgid
 |-  ( R e. Ring -> K e. ( SubRing ` R ) )
27 6 25 26 3syl
 |-  ( ph -> K e. ( SubRing ` R ) )
28 18 adantr
 |-  ( ( ph /\ x e. N ) -> W = ( Poly1 ` ( R |`s K ) ) )
29 28 fveq2d
 |-  ( ( ph /\ x e. N ) -> ( Base ` W ) = ( Base ` ( Poly1 ` ( R |`s K ) ) ) )
30 5 29 syl5eq
 |-  ( ( ph /\ x e. N ) -> B = ( Base ` ( Poly1 ` ( R |`s K ) ) ) )
31 7 30 eleqtrd
 |-  ( ( ph /\ x e. N ) -> Y e. ( Base ` ( Poly1 ` ( R |`s K ) ) ) )
32 18 eqcomd
 |-  ( ph -> ( Poly1 ` ( R |`s K ) ) = W )
33 32 fveq2d
 |-  ( ph -> ( 0g ` ( Poly1 ` ( R |`s K ) ) ) = ( 0g ` W ) )
34 33 9 eqtr4di
 |-  ( ph -> ( 0g ` ( Poly1 ` ( R |`s K ) ) ) = .0. )
35 10 34 breqtrrd
 |-  ( ph -> ( x e. N |-> Y ) finSupp ( 0g ` ( Poly1 ` ( R |`s K ) ) ) )
36 20 2 21 22 23 4 24 6 27 31 8 35 evls1gsumadd
 |-  ( ph -> ( ( R evalSub1 K ) ` ( ( Poly1 ` ( R |`s K ) ) gsum ( x e. N |-> Y ) ) ) = ( P gsum ( x e. N |-> ( ( R evalSub1 K ) ` Y ) ) ) )
37 19 36 eqtrd
 |-  ( ph -> ( ( R evalSub1 K ) ` ( W gsum ( x e. N |-> Y ) ) ) = ( P gsum ( x e. N |-> ( ( R evalSub1 K ) ` Y ) ) ) )
38 12 fveq1d
 |-  ( ph -> ( Q ` Y ) = ( ( R evalSub1 K ) ` Y ) )
39 38 eqcomd
 |-  ( ph -> ( ( R evalSub1 K ) ` Y ) = ( Q ` Y ) )
40 39 mpteq2dv
 |-  ( ph -> ( x e. N |-> ( ( R evalSub1 K ) ` Y ) ) = ( x e. N |-> ( Q ` Y ) ) )
41 40 oveq2d
 |-  ( ph -> ( P gsum ( x e. N |-> ( ( R evalSub1 K ) ` Y ) ) ) = ( P gsum ( x e. N |-> ( Q ` Y ) ) ) )
42 13 37 41 3eqtrd
 |-  ( ph -> ( Q ` ( W gsum ( x e. N |-> Y ) ) ) = ( P gsum ( x e. N |-> ( Q ` Y ) ) ) )