This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ 𝑄 = ( eval₁ ‘ 𝑅 )
		evl1gsumadd.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
		evl1gsumadd.w	⊢ 𝑊 = ( Poly₁ ‘ 𝑅 )
		evl1gsumadd.p	⊢ 𝑃 = ( 𝑅 ↑_s 𝐾 )
		evl1gsumadd.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
		evl1gsumadd.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
		evl1gsumadd.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝑌 ∈ 𝐵 )
		evl1gsumadd.n	⊢ ( 𝜑 → 𝑁 ⊆ ℕ₀ )
		evl1gsumaddval.f	⊢ ( 𝜑 → 𝑁 ∈ Fin )
		evl1gsumaddval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
	Assertion	evl1gsumaddval	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) ‘ 𝐶 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑌 ) ‘ 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evl1gsumadd.q	⊢ 𝑄 = ( eval₁ ‘ 𝑅 )
2		evl1gsumadd.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		evl1gsumadd.w	⊢ 𝑊 = ( Poly₁ ‘ 𝑅 )
4		evl1gsumadd.p	⊢ 𝑃 = ( 𝑅 ↑_s 𝐾 )
5		evl1gsumadd.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
6		evl1gsumadd.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
7		evl1gsumadd.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝑌 ∈ 𝐵 )
8		evl1gsumadd.n	⊢ ( 𝜑 → 𝑁 ⊆ ℕ₀ )
9		evl1gsumaddval.f	⊢ ( 𝜑 → 𝑁 ∈ Fin )
10		evl1gsumaddval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
11	7	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 𝑌 ∈ 𝐵 )
12	1 3 2 5 6 10 11 9	evl1gsumd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑊 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑌 ) ) ) ‘ 𝐶 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑌 ) ‘ 𝐶 ) ) ) )