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 evalSub1 R )
	evls1gsumadd.k	\|- K = ( Base ` S )
	evls1gsumadd.w	\|- W = ( Poly1 ` U )
	evls1gsumadd.0	\|- .0. = ( 0g ` W )
	evls1gsumadd.u	\|- U = ( S \|`s R )
	evls1gsumadd.p	\|- P = ( S ^s K )
	evls1gsumadd.b	\|- B = ( Base ` W )
	evls1gsumadd.s	\|- ( ph -> S e. CRing )
	evls1gsumadd.r	\|- ( ph -> R e. ( SubRing ` S ) )
	evls1gsumadd.y	\|- ( ( ph /\ x e. N ) -> Y e. B )
	evls1gsumadd.n	\|- ( ph -> N C_ NN0 )
	evls1gsumadd.f	\|- ( ph -> ( x e. N \|-> Y ) finSupp .0. )
Assertion	evls1gsumadd	\|- ( ph -> ( Q ` ( W gsum ( x e. N \|-> Y ) ) ) = ( P gsum ( x e. N \|-> ( Q ` Y ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem evls1gsumadd

Proof