gsumsmonply1

Description: A finite group sum of scaled monomials is a univariate polynomial. (Contributed by AV, 8-Oct-2019)

	Ref	Expression
Hypotheses	gsummonply1.p	\|- P = ( Poly1 ` R )
	gsummonply1.b	\|- B = ( Base ` P )
	gsummonply1.x	\|- X = ( var1 ` R )
	gsummonply1.e	\|- .^ = ( .g ` ( mulGrp ` P ) )
	gsummonply1.r	\|- ( ph -> R e. Ring )
	gsummonply1.k	\|- K = ( Base ` R )
	gsummonply1.m	\|- .* = ( .s ` P )
	gsummonply1.0	\|- .0. = ( 0g ` R )
	gsummonply1.a	\|- ( ph -> A. k e. NN0 A e. K )
	gsummonply1.f	\|- ( ph -> ( k e. NN0 \|-> A ) finSupp .0. )
Assertion	gsumsmonply1	\|- ( ph -> ( P gsum ( k e. NN0 \|-> ( A .* ( k .^ X ) ) ) ) e. B )

Proof

Step	Hyp	Ref	Expression
1		gsummonply1.p	\|- P = ( Poly1 ` R )
2		gsummonply1.b	\|- B = ( Base ` P )
3		gsummonply1.x	\|- X = ( var1 ` R )
4		gsummonply1.e	\|- .^ = ( .g ` ( mulGrp ` P ) )
5		gsummonply1.r	\|- ( ph -> R e. Ring )
6		gsummonply1.k	\|- K = ( Base ` R )
7		gsummonply1.m	\|- .* = ( .s ` P )
8		gsummonply1.0	\|- .0. = ( 0g ` R )
9		gsummonply1.a	\|- ( ph -> A. k e. NN0 A e. K )
10		gsummonply1.f	\|- ( ph -> ( k e. NN0 \|-> A ) finSupp .0. )
11		eqid	\|- ( 0g ` P ) = ( 0g ` P )
12	1	ply1ring	\|- ( R e. Ring -> P e. Ring )
13		ringcmn	\|- ( P e. Ring -> P e. CMnd )
14	5 12 13	3syl	\|- ( ph -> P e. CMnd )
15		nn0ex	\|- NN0 e. _V
16	15	a1i	\|- ( ph -> NN0 e. _V )
17	9	r19.21bi	\|- ( ( ph /\ k e. NN0 ) -> A e. K )
18	5	3ad2ant1	\|- ( ( ph /\ k e. NN0 /\ A e. K ) -> R e. Ring )
19		simp3	\|- ( ( ph /\ k e. NN0 /\ A e. K ) -> A e. K )
20		simp2	\|- ( ( ph /\ k e. NN0 /\ A e. K ) -> k e. NN0 )
21		eqid	\|- ( mulGrp ` P ) = ( mulGrp ` P )
22	6 1 3 7 21 4 2	ply1tmcl	\|- ( ( R e. Ring /\ A e. K /\ k e. NN0 ) -> ( A .* ( k .^ X ) ) e. B )
23	18 19 20 22	syl3anc	\|- ( ( ph /\ k e. NN0 /\ A e. K ) -> ( A .* ( k .^ X ) ) e. B )
24	17 23	mpd3an3	\|- ( ( ph /\ k e. NN0 ) -> ( A .* ( k .^ X ) ) e. B )
25	24	fmpttd	\|- ( ph -> ( k e. NN0 \|-> ( A .* ( k .^ X ) ) ) : NN0 --> B )
26	1	ply1lmod	\|- ( R e. Ring -> P e. LMod )
27	5 26	syl	\|- ( ph -> P e. LMod )
28	1	ply1sca	\|- ( R e. Ring -> R = ( Scalar ` P ) )
29	5 28	syl	\|- ( ph -> R = ( Scalar ` P ) )
30	1 3 21 4 2	ply1moncl	\|- ( ( R e. Ring /\ k e. NN0 ) -> ( k .^ X ) e. B )
31	5 30	sylan	\|- ( ( ph /\ k e. NN0 ) -> ( k .^ X ) e. B )
32	16 27 29 2 17 31 11 8 7 10	mptscmfsupp0	\|- ( ph -> ( k e. NN0 \|-> ( A .* ( k .^ X ) ) ) finSupp ( 0g ` P ) )
33	2 11 14 16 25 32	gsumcl	\|- ( ph -> ( P gsum ( k e. NN0 \|-> ( A .* ( k .^ X ) ) ) ) e. B )

Metamath Proof Explorer

Theorem gsumsmonply1

Proof