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 eqtrid 
 |-  ( 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 eqtrid 
 |-  ( ( 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 ) ) ) )