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	$⊢ Q = {eval}_{1} (R)$
		evl1gsumadd.k	$⊢ K = {Base}_{R}$
		evl1gsumadd.w	$⊢ W = {Poly}_{1} (R)$
		evl1gsumadd.p	$⊢ P = R ↑_{𝑠} K$
		evl1gsumadd.b	$⊢ B = {Base}_{W}$
		evl1gsumadd.r	$⊢ φ \to R \in CRing$
		evl1gsumadd.y	$⊢ (φ \land x \in N) \to Y \in B$
		evl1gsumadd.n	$⊢ φ \to N \subseteq ℕ_{0}$
		evl1gsumaddval.f	$⊢ φ \to N \in Fin$
		evl1gsumaddval.c	$⊢ φ \to C \in K$
	Assertion	evl1gsumaddval	$⊢ φ \to Q (\underset{x \in N}{\sum_{W}} Y) (C) = \underset{x \in N}{\sum_{R}} Q (Y) (C)$

Proof

Step	Hyp	Ref	Expression
1		evl1gsumadd.q	$⊢ Q = {eval}_{1} (R)$
2		evl1gsumadd.k	$⊢ K = {Base}_{R}$
3		evl1gsumadd.w	$⊢ W = {Poly}_{1} (R)$
4		evl1gsumadd.p	$⊢ P = R ↑_{𝑠} K$
5		evl1gsumadd.b	$⊢ B = {Base}_{W}$
6		evl1gsumadd.r	$⊢ φ \to R \in CRing$
7		evl1gsumadd.y	$⊢ (φ \land x \in N) \to Y \in B$
8		evl1gsumadd.n	$⊢ φ \to N \subseteq ℕ_{0}$
9		evl1gsumaddval.f	$⊢ φ \to N \in Fin$
10		evl1gsumaddval.c	$⊢ φ \to C \in K$
11	7	ralrimiva	$⊢ φ \to \forall x \in N Y \in B$
12	1 3 2 5 6 10 11 9	evl1gsumd	$⊢ φ \to Q (\underset{x \in N}{\sum_{W}} Y) (C) = \underset{x \in N}{\sum_{R}} Q (Y) (C)$