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 𝑄 = ( eval1𝑅 )
evl1gsumadd.k 𝐾 = ( Base ‘ 𝑅 )
evl1gsumadd.w 𝑊 = ( Poly1𝑅 )
evl1gsumadd.p 𝑃 = ( 𝑅s 𝐾 )
evl1gsumadd.b 𝐵 = ( Base ‘ 𝑊 )
evl1gsumadd.r ( 𝜑𝑅 ∈ CRing )
evl1gsumadd.y ( ( 𝜑𝑥𝑁 ) → 𝑌𝐵 )
evl1gsumadd.n ( 𝜑𝑁 ⊆ ℕ0 )
evl1gsumadd.0 0 = ( 0g𝑊 )
evl1gsumadd.f ( 𝜑 → ( 𝑥𝑁𝑌 ) finSupp 0 )
Assertion evl1gsumadd ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 evl1gsumadd.q 𝑄 = ( eval1𝑅 )
2 evl1gsumadd.k 𝐾 = ( Base ‘ 𝑅 )
3 evl1gsumadd.w 𝑊 = ( Poly1𝑅 )
4 evl1gsumadd.p 𝑃 = ( 𝑅s 𝐾 )
5 evl1gsumadd.b 𝐵 = ( Base ‘ 𝑊 )
6 evl1gsumadd.r ( 𝜑𝑅 ∈ CRing )
7 evl1gsumadd.y ( ( 𝜑𝑥𝑁 ) → 𝑌𝐵 )
8 evl1gsumadd.n ( 𝜑𝑁 ⊆ ℕ0 )
9 evl1gsumadd.0 0 = ( 0g𝑊 )
10 evl1gsumadd.f ( 𝜑 → ( 𝑥𝑁𝑌 ) finSupp 0 )
11 1 2 evl1fval1 𝑄 = ( 𝑅 evalSub1 𝐾 )
12 11 a1i ( 𝜑𝑄 = ( 𝑅 evalSub1 𝐾 ) )
13 12 fveq1d ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) = ( ( 𝑅 evalSub1 𝐾 ) ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) )
14 2 ressid ( 𝑅 ∈ CRing → ( 𝑅s 𝐾 ) = 𝑅 )
15 6 14 syl ( 𝜑 → ( 𝑅s 𝐾 ) = 𝑅 )
16 15 eqcomd ( 𝜑𝑅 = ( 𝑅s 𝐾 ) )
17 16 fveq2d ( 𝜑 → ( Poly1𝑅 ) = ( Poly1 ‘ ( 𝑅s 𝐾 ) ) )
18 3 17 syl5eq ( 𝜑𝑊 = ( Poly1 ‘ ( 𝑅s 𝐾 ) ) )
19 18 fvoveq1d ( 𝜑 → ( ( 𝑅 evalSub1 𝐾 ) ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) = ( ( 𝑅 evalSub1 𝐾 ) ‘ ( ( Poly1 ‘ ( 𝑅s 𝐾 ) ) Σg ( 𝑥𝑁𝑌 ) ) ) )
20 eqid ( 𝑅 evalSub1 𝐾 ) = ( 𝑅 evalSub1 𝐾 )
21 eqid ( Poly1 ‘ ( 𝑅s 𝐾 ) ) = ( Poly1 ‘ ( 𝑅s 𝐾 ) )
22 eqid ( 0g ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) ) = ( 0g ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) )
23 eqid ( 𝑅s 𝐾 ) = ( 𝑅s 𝐾 )
24 eqid ( Base ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) )
25 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
26 2 subrgid ( 𝑅 ∈ Ring → 𝐾 ∈ ( SubRing ‘ 𝑅 ) )
27 6 25 26 3syl ( 𝜑𝐾 ∈ ( SubRing ‘ 𝑅 ) )
28 18 adantr ( ( 𝜑𝑥𝑁 ) → 𝑊 = ( Poly1 ‘ ( 𝑅s 𝐾 ) ) )
29 28 fveq2d ( ( 𝜑𝑥𝑁 ) → ( Base ‘ 𝑊 ) = ( Base ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) ) )
30 5 29 syl5eq ( ( 𝜑𝑥𝑁 ) → 𝐵 = ( Base ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) ) )
31 7 30 eleqtrd ( ( 𝜑𝑥𝑁 ) → 𝑌 ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) ) )
32 18 eqcomd ( 𝜑 → ( Poly1 ‘ ( 𝑅s 𝐾 ) ) = 𝑊 )
33 32 fveq2d ( 𝜑 → ( 0g ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) ) = ( 0g𝑊 ) )
34 33 9 eqtr4di ( 𝜑 → ( 0g ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) ) = 0 )
35 10 34 breqtrrd ( 𝜑 → ( 𝑥𝑁𝑌 ) finSupp ( 0g ‘ ( Poly1 ‘ ( 𝑅s 𝐾 ) ) ) )
36 20 2 21 22 23 4 24 6 27 31 8 35 evls1gsumadd ( 𝜑 → ( ( 𝑅 evalSub1 𝐾 ) ‘ ( ( Poly1 ‘ ( 𝑅s 𝐾 ) ) Σg ( 𝑥𝑁𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥𝑁 ↦ ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) ) ) )
37 19 36 eqtrd ( 𝜑 → ( ( 𝑅 evalSub1 𝐾 ) ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥𝑁 ↦ ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) ) ) )
38 12 fveq1d ( 𝜑 → ( 𝑄𝑌 ) = ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) )
39 38 eqcomd ( 𝜑 → ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) = ( 𝑄𝑌 ) )
40 39 mpteq2dv ( 𝜑 → ( 𝑥𝑁 ↦ ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) ) = ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) )
41 40 oveq2d ( 𝜑 → ( 𝑃 Σg ( 𝑥𝑁 ↦ ( ( 𝑅 evalSub1 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) )
42 13 37 41 3eqtrd ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) = ( 𝑃 Σg ( 𝑥𝑁 ↦ ( 𝑄𝑌 ) ) ) )