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 8 15	mplringd	\|- ( ph -> W e. Ring )
17		ringcmn	\|- ( W e. Ring -> W e. CMnd )
18	16 17	syl	\|- ( ph -> W e. CMnd )
19		crngring	\|- ( S e. CRing -> S e. Ring )
20	9 19	syl	\|- ( ph -> S e. Ring )
21		ovex	\|- ( K ^m I ) e. _V
22	20 21	jctir	\|- ( ph -> ( S e. Ring /\ ( K ^m I ) e. _V ) )
23	5	pwsring	\|- ( ( S e. Ring /\ ( K ^m I ) e. _V ) -> P e. Ring )
24		ringmnd	\|- ( P e. Ring -> P e. Mnd )
25	22 23 24	3syl	\|- ( ph -> P e. Mnd )
26		nn0ex	\|- NN0 e. _V
27	26	a1i	\|- ( ph -> NN0 e. _V )
28	27 12	ssexd	\|- ( ph -> N e. _V )
29	1 2 4 5 6	evlsrhm	\|- ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom P ) )
30	8 9 10 29	syl3anc	\|- ( ph -> Q e. ( W RingHom P ) )
31		rhmghm	\|- ( Q e. ( W RingHom P ) -> Q e. ( W GrpHom P ) )
32		ghmmhm	\|- ( Q e. ( W GrpHom P ) -> Q e. ( W MndHom P ) )
33	30 31 32	3syl	\|- ( ph -> Q e. ( W MndHom P ) )
34	7 3 18 25 28 33 11 13	gsummptmhm	\|- ( ph -> ( P gsum ( x e. N \|-> ( Q ` Y ) ) ) = ( Q ` ( W gsum ( x e. N \|-> Y ) ) ) )
35	34	eqcomd	\|- ( ph -> ( Q ` ( W gsum ( x e. N \|-> Y ) ) ) = ( P gsum ( x e. N \|-> ( Q ` Y ) ) ) )

Metamath Proof Explorer

Theorem evlsgsumadd

Proof