Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Univariate polynomial evaluation
evl1gsumaddval
Metamath Proof Explorer
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 ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑌 ) ‘ 𝐶 ) ) ) )