Metamath Proof Explorer


Theorem evl1gsumaddval

Description: Value of a univariate polynomial evaluation mapping an additive group sum to a group sum of the evaluated variable. (Contributed by AV, 17-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 )
evl1gsumaddval.f ( 𝜑𝑁 ∈ Fin )
evl1gsumaddval.c ( 𝜑𝐶𝐾 )
Assertion evl1gsumaddval ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σ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 evl1gsumaddval.f ( 𝜑𝑁 ∈ Fin )
10 evl1gsumaddval.c ( 𝜑𝐶𝐾 )
11 7 ralrimiva ( 𝜑 → ∀ 𝑥𝑁 𝑌𝐵 )
12 1 3 2 5 6 10 11 9 evl1gsumd ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σg ( 𝑥𝑁𝑌 ) ) ) ‘ 𝐶 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑄𝑌 ) ‘ 𝐶 ) ) ) )