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

Metamath Proof Explorer

Theorem evls1gsumadd

Proof