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

Proof

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

Metamath Proof Explorer

Theorem evls1gsummul

Proof