evls1gsummul

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

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

Proof

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

Metamath Proof Explorer

Theorem evls1gsummul

Proof