evls1gsumadd

Description: Univariate polynomial evaluation maps (additive) group sums to group sums. (Contributed by AV, 14-Sep-2019)

	Ref	Expression
Hypotheses	evls1gsumadd.q	$⊢ Q = S {evalSub}_{1} R$
	evls1gsumadd.k	$⊢ K = {Base}_{S}$
	evls1gsumadd.w	$⊢ W = {Poly}_{1} (U)$
	evls1gsumadd.0	$⊢ \underset{˙}{0} = 0_{W}$
	evls1gsumadd.u	$⊢ U = S ↾_{𝑠} R$
	evls1gsumadd.p	$⊢ P = S ↑_{𝑠} K$
	evls1gsumadd.b	$⊢ B = {Base}_{W}$
	evls1gsumadd.s	$⊢ φ \to S \in CRing$
	evls1gsumadd.r	$⊢ φ \to R \in SubRing (S)$
	evls1gsumadd.y	$⊢ (φ \land x \in N) \to Y \in B$
	evls1gsumadd.n	$⊢ φ \to N \subseteq ℕ_{0}$
	evls1gsumadd.f	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in N ⟼ Y))$
Assertion	evls1gsumadd	$⊢ φ \to Q (\underset{x \in N}{\sum_{W}} Y) = \underset{x \in N}{\sum_{P}} Q (Y)$

Proof

Step	Hyp	Ref	Expression
1		evls1gsumadd.q	$⊢ Q = S {evalSub}_{1} R$
2		evls1gsumadd.k	$⊢ K = {Base}_{S}$
3		evls1gsumadd.w	$⊢ W = {Poly}_{1} (U)$
4		evls1gsumadd.0	$⊢ \underset{˙}{0} = 0_{W}$
5		evls1gsumadd.u	$⊢ U = S ↾_{𝑠} R$
6		evls1gsumadd.p	$⊢ P = S ↑_{𝑠} K$
7		evls1gsumadd.b	$⊢ B = {Base}_{W}$
8		evls1gsumadd.s	$⊢ φ \to S \in CRing$
9		evls1gsumadd.r	$⊢ φ \to R \in SubRing (S)$
10		evls1gsumadd.y	$⊢ (φ \land x \in N) \to Y \in B$
11		evls1gsumadd.n	$⊢ φ \to N \subseteq ℕ_{0}$
12		evls1gsumadd.f	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in N ⟼ Y))$
13	5	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
14	9 13	syl	$⊢ φ \to U \in Ring$
15	3	ply1ring	$⊢ U \in Ring \to W \in Ring$
16		ringcmn	$⊢ W \in Ring \to W \in CMnd$
17	14 15 16	3syl	$⊢ φ \to W \in CMnd$
18		crngring	$⊢ S \in CRing \to S \in Ring$
19	8 18	syl	$⊢ φ \to S \in Ring$
20	2	fvexi	$⊢ K \in V$
21	19 20	jctir	$⊢ φ \to (S \in Ring \land K \in V)$
22	6	pwsring	$⊢ (S \in Ring \land K \in V) \to P \in Ring$
23		ringmnd	$⊢ P \in Ring \to P \in Mnd$
24	21 22 23	3syl	$⊢ φ \to P \in Mnd$
25		nn0ex	$⊢ ℕ_{0} \in V$
26	25	a1i	$⊢ φ \to ℕ_{0} \in V$
27	26 11	ssexd	$⊢ φ \to N \in V$
28	1 2 6 5 3	evls1rhm	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom P)$
29	8 9 28	syl2anc	$⊢ φ \to Q \in (W RingHom P)$
30		rhmghm	$⊢ Q \in (W RingHom P) \to Q \in (W GrpHom P)$
31		ghmmhm	$⊢ Q \in (W GrpHom P) \to Q \in (W MndHom P)$
32	29 30 31	3syl	$⊢ φ \to Q \in (W MndHom P)$
33	7 4 17 24 27 32 10 12	gsummptmhm	$⊢ φ \to \underset{x \in N}{\sum_{P}} Q (Y) = Q (\underset{x \in N}{\sum_{W}} Y)$
34	33	eqcomd	$⊢ φ \to Q (\underset{x \in N}{\sum_{W}} Y) = \underset{x \in N}{\sum_{P}} Q (Y)$

Metamath Proof Explorer

Theorem evls1gsumadd

Proof