Theorem ply1mulgsum

Description: The product of two polynomials expressed as group sum of scaled monomials. (Contributed by AV, 20-Oct-2019)

	Ref	Expression
Hypotheses	ply1mulgsum.p	|- P = ( Poly1 ` R )
	ply1mulgsum.b	|- B = ( Base ` P )
	ply1mulgsum.a	|- A = ( coe1 ` K )
	ply1mulgsum.c	|- C = ( coe1 ` L )
	ply1mulgsum.x	|- X = ( var1 ` R )
	ply1mulgsum.pm	|- .X. = ( .r ` P )
	ply1mulgsum.sm	|- .x. = ( .s ` P )
	ply1mulgsum.rm	|- .* = ( .r ` R )
	ply1mulgsum.m	|- M = ( mulGrp ` P )
	ply1mulgsum.e	|- .^ = ( .g ` M )
Assertion	ply1mulgsum	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( K .X. L ) = ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1mulgsum.p	|- P = ( Poly1 ` R )
2		ply1mulgsum.b	|- B = ( Base ` P )
3		ply1mulgsum.a	|- A = ( coe1 ` K )
4		ply1mulgsum.c	|- C = ( coe1 ` L )
5		ply1mulgsum.x	|- X = ( var1 ` R )
6		ply1mulgsum.pm	|- .X. = ( .r ` P )
7		ply1mulgsum.sm	|- .x. = ( .s ` P )
8		ply1mulgsum.rm	|- .* = ( .r ` R )
9		ply1mulgsum.m	|- M = ( mulGrp ` P )
10		ply1mulgsum.e	|- .^ = ( .g ` M )
11	1 6 8 2	coe1mul	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( coe1 ` ( K .X. L ) ) = ( m e. NN0 |-> ( R gsum ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) ) ) )
12	11	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( coe1 ` ( K .X. L ) ) = ( m e. NN0 |-> ( R gsum ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) ) ) )
13	12	fveq1d	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( ( coe1 ` ( K .X. L ) ) ` n ) = ( ( m e. NN0 |-> ( R gsum ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) ) ) ` n ) )
14		eqidd	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( m e. NN0 |-> ( R gsum ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) ) ) = ( m e. NN0 |-> ( R gsum ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) ) ) )
15		oveq2	|- ( m = n -> ( 0 ... m ) = ( 0 ... n ) )
16		fvoveq1	|- ( m = n -> ( ( coe1 ` L ) ` ( m - i ) ) = ( ( coe1 ` L ) ` ( n - i ) ) )
17	16	oveq2d	|- ( m = n -> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) = ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) )
18	15 17	mpteq12dv	|- ( m = n -> ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) = ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) ) )
19	18	oveq2d	|- ( m = n -> ( R gsum ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) ) = ( R gsum ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) ) ) )
20	19	adantl	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ m = n ) -> ( R gsum ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) ) = ( R gsum ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) ) ) )
21		simpr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> n e. NN0 )
22		ovexd	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( R gsum ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) ) ) e. _V )
23	14 20 21 22	fvmptd	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( ( m e. NN0 |-> ( R gsum ( i e. ( 0 ... m ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( m - i ) ) ) ) ) ) ` n ) = ( R gsum ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) ) ) )
24	9	fveq2i	|- ( .g ` M ) = ( .g ` ( mulGrp ` P ) )
25	10 24	eqtri	|- .^ = ( .g ` ( mulGrp ` P ) )
26		simp1	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> R e. Ring )
27	26	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> R e. Ring )
28		eqid	|- ( Base ` R ) = ( Base ` R )
29		eqid	|- ( 0g ` R ) = ( 0g ` R )
30		ringcmn	|- ( R e. Ring -> R e. CMnd )
31	30	3ad2ant1	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> R e. CMnd )
32	31	ad2antrr	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) -> R e. CMnd )
33		fzfid	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) -> ( 0 ... k ) e. Fin )
34		simpll1	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) -> R e. Ring )
35	34	adantr	|- ( ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> R e. Ring )
36		simp2	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> K e. B )
37	36	ad2antrr	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) -> K e. B )
38		elfznn0	|- ( l e. ( 0 ... k ) -> l e. NN0 )
39	3 2 1 28	coe1fvalcl	|- ( ( K e. B /\ l e. NN0 ) -> ( A ` l ) e. ( Base ` R ) )
40	37 38 39	syl2an	|- ( ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> ( A ` l ) e. ( Base ` R ) )
41		simp3	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> L e. B )
42	41	ad2antrr	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) -> L e. B )
43		fznn0sub	|- ( l e. ( 0 ... k ) -> ( k - l ) e. NN0 )
44	4 2 1 28	coe1fvalcl	|- ( ( L e. B /\ ( k - l ) e. NN0 ) -> ( C ` ( k - l ) ) e. ( Base ` R ) )
45	42 43 44	syl2an	|- ( ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> ( C ` ( k - l ) ) e. ( Base ` R ) )
46	28 8	ringcl	|- ( ( R e. Ring /\ ( A ` l ) e. ( Base ` R ) /\ ( C ` ( k - l ) ) e. ( Base ` R ) ) -> ( ( A ` l ) .* ( C ` ( k - l ) ) ) e. ( Base ` R ) )
47	35 40 45 46	syl3anc	|- ( ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> ( ( A ` l ) .* ( C ` ( k - l ) ) ) e. ( Base ` R ) )
48	47	ralrimiva	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) -> A. l e. ( 0 ... k ) ( ( A ` l ) .* ( C ` ( k - l ) ) ) e. ( Base ` R ) )
49	28 32 33 48	gsummptcl	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) /\ k e. NN0 ) -> ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) e. ( Base ` R ) )
50	49	ralrimiva	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> A. k e. NN0 ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) e. ( Base ` R ) )
51	1 2 3 4 5 6 7 8 9 10	ply1mulgsumlem3	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( k e. NN0 |-> ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) ) finSupp ( 0g ` R ) )
52	51	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( k e. NN0 |-> ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) ) finSupp ( 0g ` R ) )
53	1 2 5 25 27 28 7 29 50 52 21	gsummoncoe1	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) ` n ) = [_ n / k ]_ ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) )
54		vex	|- n e. _V
55		csbov2g	|- ( n e. _V -> [_ n / k ]_ ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) = ( R gsum [_ n / k ]_ ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) )
56		id	|- ( n e. _V -> n e. _V )
57		oveq2	|- ( k = n -> ( 0 ... k ) = ( 0 ... n ) )
58		fvoveq1	|- ( k = n -> ( C ` ( k - l ) ) = ( C ` ( n - l ) ) )
59	58	oveq2d	|- ( k = n -> ( ( A ` l ) .* ( C ` ( k - l ) ) ) = ( ( A ` l ) .* ( C ` ( n - l ) ) ) )
60	57 59	mpteq12dv	|- ( k = n -> ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
61	60	adantl	|- ( ( n e. _V /\ k = n ) -> ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
62	56 61	csbied	|- ( n e. _V -> [_ n / k ]_ ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
63	62	oveq2d	|- ( n e. _V -> ( R gsum [_ n / k ]_ ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) = ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) )
64	55 63	eqtrd	|- ( n e. _V -> [_ n / k ]_ ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) = ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) )
65	54 64	mp1i	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> [_ n / k ]_ ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) = ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) )
66		fveq2	|- ( l = i -> ( A ` l ) = ( A ` i ) )
67	3	fveq1i	|- ( A ` i ) = ( ( coe1 ` K ) ` i )
68	66 67	eqtrdi	|- ( l = i -> ( A ` l ) = ( ( coe1 ` K ) ` i ) )
69		oveq2	|- ( l = i -> ( n - l ) = ( n - i ) )
70	69	fveq2d	|- ( l = i -> ( C ` ( n - l ) ) = ( C ` ( n - i ) ) )
71	4	fveq1i	|- ( C ` ( n - i ) ) = ( ( coe1 ` L ) ` ( n - i ) )
72	70 71	eqtrdi	|- ( l = i -> ( C ` ( n - l ) ) = ( ( coe1 ` L ) ` ( n - i ) ) )
73	68 72	oveq12d	|- ( l = i -> ( ( A ` l ) .* ( C ` ( n - l ) ) ) = ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) )
74	73	cbvmptv	|- ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) = ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) )
75	74	a1i	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) = ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) ) )
76	75	oveq2d	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( R gsum ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) ) ) )
77	53 65 76	3eqtrrd	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( R gsum ( i e. ( 0 ... n ) |-> ( ( ( coe1 ` K ) ` i ) .* ( ( coe1 ` L ) ` ( n - i ) ) ) ) ) = ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) ` n ) )
78	13 23 77	3eqtrd	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ n e. NN0 ) -> ( ( coe1 ` ( K .X. L ) ) ` n ) = ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) ` n ) )
79	78	ralrimiva	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> A. n e. NN0 ( ( coe1 ` ( K .X. L ) ) ` n ) = ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) ` n ) )
80	1	ply1ring	|- ( R e. Ring -> P e. Ring )
81	2 6	ringcl	|- ( ( P e. Ring /\ K e. B /\ L e. B ) -> ( K .X. L ) e. B )
82	80 81	syl3an1	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( K .X. L ) e. B )
83		eqid	|- ( 0g ` P ) = ( 0g ` P )
84		ringcmn	|- ( P e. Ring -> P e. CMnd )
85	80 84	syl	|- ( R e. Ring -> P e. CMnd )
86	85	3ad2ant1	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> P e. CMnd )
87		nn0ex	|- NN0 e. _V
88	87	a1i	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> NN0 e. _V )
89	1	ply1lmod	|- ( R e. Ring -> P e. LMod )
90	89	3ad2ant1	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> P e. LMod )
91	90	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> P e. LMod )
92	31	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> R e. CMnd )
93		fzfid	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> ( 0 ... k ) e. Fin )
94		simpll1	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> R e. Ring )
95	36	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> K e. B )
96	95 38 39	syl2an	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> ( A ` l ) e. ( Base ` R ) )
97	41	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> L e. B )
98	97 43 44	syl2an	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> ( C ` ( k - l ) ) e. ( Base ` R ) )
99	94 96 98 46	syl3anc	|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> ( ( A ` l ) .* ( C ` ( k - l ) ) ) e. ( Base ` R ) )
100	99	ralrimiva	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> A. l e. ( 0 ... k ) ( ( A ` l ) .* ( C ` ( k - l ) ) ) e. ( Base ` R ) )
101	28 92 93 100	gsummptcl	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) e. ( Base ` R ) )
102	26	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> R e. Ring )
103	1	ply1sca	|- ( R e. Ring -> R = ( Scalar ` P ) )
104	102 103	syl	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> R = ( Scalar ` P ) )
105	104	fveq2d	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
106	101 105	eleqtrd	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) e. ( Base ` ( Scalar ` P ) ) )
107	9 2	mgpbas	|- B = ( Base ` M )
108	9	ringmgp	|- ( P e. Ring -> M e. Mnd )
109	80 108	syl	|- ( R e. Ring -> M e. Mnd )
110	109	3ad2ant1	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> M e. Mnd )
111	110	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> M e. Mnd )
112		simpr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> k e. NN0 )
113	5 1 2	vr1cl	|- ( R e. Ring -> X e. B )
114	113	3ad2ant1	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> X e. B )
115	114	adantr	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> X e. B )
116	107 10 111 112 115	mulgnn0cld	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> ( k .^ X ) e. B )
117		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
118		eqid	|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
119	2 117 7 118	lmodvscl	|- ( ( P e. LMod /\ ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) e. ( Base ` ( Scalar ` P ) ) /\ ( k .^ X ) e. B ) -> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) e. B )
120	91 106 116 119	syl3anc	|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) e. B )
121	120	fmpttd	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) : NN0 --> B )
122	1 2 3 4 5 6 7 8 9 10	ply1mulgsumlem4	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) finSupp ( 0g ` P ) )
123	2 83 86 88 121 122	gsumcl	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) e. B )
124		eqid	|- ( coe1 ` ( K .X. L ) ) = ( coe1 ` ( K .X. L ) )
125		eqid	|- ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) = ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) )
126	1 2 124 125	ply1coe1eq	|- ( ( R e. Ring /\ ( K .X. L ) e. B /\ ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) e. B ) -> ( A. n e. NN0 ( ( coe1 ` ( K .X. L ) ) ` n ) = ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) ` n ) <-> ( K .X. L ) = ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) )
127	26 82 123 126	syl3anc	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. n e. NN0 ( ( coe1 ` ( K .X. L ) ) ` n ) = ( ( coe1 ` ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) ` n ) <-> ( K .X. L ) = ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) ) )
128	79 127	mpbid	|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( K .X. L ) = ( P gsum ( k e. NN0 |-> ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) ) ) )