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 ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑌 ) ‘ 𝐶 ) ) ) )