Metamath Proof Explorer

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 ringmgp 
 |-  ( P e. Ring -> M e. Mnd )
108 80 107 syl 
 |-  ( R e. Ring -> M e. Mnd )
109 108 3ad2ant1 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> M e. Mnd )
110 109 adantr 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> M e. Mnd )
111 simpr 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> k e. NN0 )
112 5 1 2 vr1cl 
 |-  ( R e. Ring -> X e. B )
113 112 3ad2ant1 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> X e. B )
114 113 adantr 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> X e. B )
115 9 2 mgpbas 
 |-  B = ( Base ` M )
116 115 10 mulgnn0cl 
 |-  ( ( M e. Mnd /\ k e. NN0 /\ X e. B ) -> ( k .^ X ) e. B )
117 110 111 114 116 syl3anc 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ k e. NN0 ) -> ( k .^ X ) e. B )
118 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
119 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
120 2 118 7 119 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 )
121 91 106 117 120 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 )
122 121 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 )
123 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 ) )
124 2 83 86 88 122 123 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 )
125 eqid 
 |-  ( coe1 ` ( K .X. L ) ) = ( coe1 ` ( K .X. L ) )
126 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 ) ) ) ) )
127 1 2 125 126 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 ) ) ) ) ) )
128 26 82 124 127 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 ) ) ) ) ) )
129 79 128 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 ) ) ) ) )