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	3	ply1ring	$⊢ U \in Ring \to W \in Ring$
15		ringcmn	$⊢ W \in Ring \to W \in CMnd$
16	9 13 14 15	4syl	$⊢ φ \to W \in CMnd$
17		crngring	$⊢ S \in CRing \to S \in Ring$
18	8 17	syl	$⊢ φ \to S \in Ring$
19	2	fvexi	$⊢ K \in V$
20	18 19	jctir	$⊢ φ \to (S \in Ring \land K \in V)$
21	6	pwsring	$⊢ (S \in Ring \land K \in V) \to P \in Ring$
22		ringmnd	$⊢ P \in Ring \to P \in Mnd$
23	20 21 22	3syl	$⊢ φ \to P \in Mnd$
24		nn0ex	$⊢ ℕ_{0} \in V$
25	24	a1i	$⊢ φ \to ℕ_{0} \in V$
26	25 11	ssexd	$⊢ φ \to N \in V$
27	1 2 6 5 3	evls1rhm	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom P)$
28	8 9 27	syl2anc	$⊢ φ \to Q \in (W RingHom P)$
29		rhmghm	$⊢ Q \in (W RingHom P) \to Q \in (W GrpHom P)$
30		ghmmhm	$⊢ Q \in (W GrpHom P) \to Q \in (W MndHom P)$
31	28 29 30	3syl	$⊢ φ \to Q \in (W MndHom P)$
32	7 4 16 23 26 31 10 12	gsummptmhm	$⊢ φ \to \underset{x \in N}{\sum_{P}} Q (Y) = Q (\underset{x \in N}{\sum_{W}} Y)$
33	32	eqcomd	$⊢ φ \to Q (\underset{x \in N}{\sum_{W}} Y) = \underset{x \in N}{\sum_{P}} Q (Y)$

Metamath Proof Explorer

Theorem evls1gsumadd

Proof