evlsgsumadd

Description: Polynomial evaluation maps (additive) group sums to group sums. (Contributed by SN, 13-Feb-2024)

	Ref	Expression
Hypotheses	evlsgsumadd.q	\|- Q = ( ( I evalSub S ) ` R )
	evlsgsumadd.w	\|- W = ( I mPoly U )
	evlsgsumadd.0	\|- .0. = ( 0g ` W )
	evlsgsumadd.u	\|- U = ( S \|`s R )
	evlsgsumadd.p	\|- P = ( S ^s ( K ^m I ) )
	evlsgsumadd.k	\|- K = ( Base ` S )
	evlsgsumadd.b	\|- B = ( Base ` W )
	evlsgsumadd.i	\|- ( ph -> I e. V )
	evlsgsumadd.s	\|- ( ph -> S e. CRing )
	evlsgsumadd.r	\|- ( ph -> R e. ( SubRing ` S ) )
	evlsgsumadd.y	\|- ( ( ph /\ x e. N ) -> Y e. B )
	evlsgsumadd.n	\|- ( ph -> N C_ NN0 )
	evlsgsumadd.f	\|- ( ph -> ( x e. N \|-> Y ) finSupp .0. )
Assertion	evlsgsumadd	\|- ( ph -> ( Q ` ( W gsum ( x e. N \|-> Y ) ) ) = ( P gsum ( x e. N \|-> ( Q ` Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsgsumadd.q	\|- Q = ( ( I evalSub S ) ` R )
2		evlsgsumadd.w	\|- W = ( I mPoly U )
3		evlsgsumadd.0	\|- .0. = ( 0g ` W )
4		evlsgsumadd.u	\|- U = ( S \|`s R )
5		evlsgsumadd.p	\|- P = ( S ^s ( K ^m I ) )
6		evlsgsumadd.k	\|- K = ( Base ` S )
7		evlsgsumadd.b	\|- B = ( Base ` W )
8		evlsgsumadd.i	\|- ( ph -> I e. V )
9		evlsgsumadd.s	\|- ( ph -> S e. CRing )
10		evlsgsumadd.r	\|- ( ph -> R e. ( SubRing ` S ) )
11		evlsgsumadd.y	\|- ( ( ph /\ x e. N ) -> Y e. B )
12		evlsgsumadd.n	\|- ( ph -> N C_ NN0 )
13		evlsgsumadd.f	\|- ( ph -> ( x e. N \|-> Y ) finSupp .0. )
14	4	subrgring	\|- ( R e. ( SubRing ` S ) -> U e. Ring )
15	10 14	syl	\|- ( ph -> U e. Ring )
16	2	mplring	\|- ( ( I e. V /\ U e. Ring ) -> W e. Ring )
17	8 15 16	syl2anc	\|- ( ph -> W e. Ring )
18		ringcmn	\|- ( W e. Ring -> W e. CMnd )
19	17 18	syl	\|- ( ph -> W e. CMnd )
20		crngring	\|- ( S e. CRing -> S e. Ring )
21	9 20	syl	\|- ( ph -> S e. Ring )
22		ovex	\|- ( K ^m I ) e. _V
23	21 22	jctir	\|- ( ph -> ( S e. Ring /\ ( K ^m I ) e. _V ) )
24	5	pwsring	\|- ( ( S e. Ring /\ ( K ^m I ) e. _V ) -> P e. Ring )
25		ringmnd	\|- ( P e. Ring -> P e. Mnd )
26	23 24 25	3syl	\|- ( ph -> P e. Mnd )
27		nn0ex	\|- NN0 e. _V
28	27	a1i	\|- ( ph -> NN0 e. _V )
29	28 12	ssexd	\|- ( ph -> N e. _V )
30	1 2 4 5 6	evlsrhm	\|- ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom P ) )
31	8 9 10 30	syl3anc	\|- ( ph -> Q e. ( W RingHom P ) )
32		rhmghm	\|- ( Q e. ( W RingHom P ) -> Q e. ( W GrpHom P ) )
33		ghmmhm	\|- ( Q e. ( W GrpHom P ) -> Q e. ( W MndHom P ) )
34	31 32 33	3syl	\|- ( ph -> Q e. ( W MndHom P ) )
35	7 3 19 26 29 34 11 13	gsummptmhm	\|- ( ph -> ( P gsum ( x e. N \|-> ( Q ` Y ) ) ) = ( Q ` ( W gsum ( x e. N \|-> Y ) ) ) )
36	35	eqcomd	\|- ( ph -> ( Q ` ( W gsum ( x e. N \|-> Y ) ) ) = ( P gsum ( x e. N \|-> ( Q ` Y ) ) ) )

Metamath Proof Explorer

Theorem evlsgsumadd

Proof