Metamath Proof Explorer

Theorem ply1mulgsumlem4

Description: Lemma 4 for ply1mulgsum . (Contributed by AV, 19-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 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 ) )

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 fvexd 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( 0g ` P ) e. _V )
12 ovexd 
 |-  ( ( ( 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. _V )
13 1 2 3 4 5 6 7 8 9 10 ply1mulgsumlem2 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) )
14 vex 
 |-  n e. _V
15 csbov12g 
 |-  ( n e. _V -> [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( [_ n / k ]_ ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. [_ n / k ]_ ( k .^ X ) ) )
16 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 ) ) ) ) ) )
17 id 
 |-  ( n e. _V -> n e. _V )
18 oveq2 
 |-  ( k = n -> ( 0 ... k ) = ( 0 ... n ) )
19 fvoveq1 
 |-  ( k = n -> ( C ` ( k - l ) ) = ( C ` ( n - l ) ) )
20 19 oveq2d 
 |-  ( k = n -> ( ( A ` l ) .* ( C ` ( k - l ) ) ) = ( ( A ` l ) .* ( C ` ( n - l ) ) ) )
21 18 20 mpteq12dv 
 |-  ( k = n -> ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
22 21 adantl 
 |-  ( ( n e. _V /\ k = n ) -> ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
23 17 22 csbied 
 |-  ( n e. _V -> [_ n / k ]_ ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
24 23 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 ) ) ) ) ) )
25 16 24 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 ) ) ) ) ) )
26 csbov1g 
 |-  ( n e. _V -> [_ n / k ]_ ( k .^ X ) = ( [_ n / k ]_ k .^ X ) )
27 csbvarg 
 |-  ( n e. _V -> [_ n / k ]_ k = n )
28 27 oveq1d 
 |-  ( n e. _V -> ( [_ n / k ]_ k .^ X ) = ( n .^ X ) )
29 26 28 eqtrd 
 |-  ( n e. _V -> [_ n / k ]_ ( k .^ X ) = ( n .^ X ) )
30 25 29 oveq12d 
 |-  ( n e. _V -> ( [_ n / k ]_ ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. [_ n / k ]_ ( k .^ X ) ) = ( ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) .x. ( n .^ X ) ) )
31 15 30 eqtrd 
 |-  ( n e. _V -> [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) .x. ( n .^ X ) ) )
32 14 31 ax-mp 
 |-  [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) .x. ( n .^ X ) )
33 oveq1 
 |-  ( ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) -> ( ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) .x. ( n .^ X ) ) = ( ( 0g ` R ) .x. ( n .^ X ) ) )
34 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
35 34 3ad2ant1 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> R = ( Scalar ` P ) )
36 35 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> R = ( Scalar ` P ) )
37 36 fveq2d 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
38 37 oveq1d 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( ( 0g ` R ) .x. ( n .^ X ) ) = ( ( 0g ` ( Scalar ` P ) ) .x. ( n .^ X ) ) )
39 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
40 39 3ad2ant1 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> P e. LMod )
41 40 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> P e. LMod )
42 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
43 9 ringmgp 
 |-  ( P e. Ring -> M e. Mnd )
44 42 43 syl 
 |-  ( R e. Ring -> M e. Mnd )
45 44 3ad2ant1 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> M e. Mnd )
46 45 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> M e. Mnd )
47 simpr 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> n e. NN0 )
48 5 1 2 vr1cl 
 |-  ( R e. Ring -> X e. B )
49 48 3ad2ant1 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> X e. B )
50 49 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> X e. B )
51 9 2 mgpbas 
 |-  B = ( Base ` M )
52 51 10 mulgnn0cl 
 |-  ( ( M e. Mnd /\ n e. NN0 /\ X e. B ) -> ( n .^ X ) e. B )
53 46 47 50 52 syl3anc 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( n .^ X ) e. B )
54 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
55 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
56 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
57 2 54 7 55 56 lmod0vs 
 |-  ( ( P e. LMod /\ ( n .^ X ) e. B ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( n .^ X ) ) = ( 0g ` P ) )
58 41 53 57 syl2anc 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( n .^ X ) ) = ( 0g ` P ) )
59 38 58 eqtrd 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( ( 0g ` R ) .x. ( n .^ X ) ) = ( 0g ` P ) )
60 33 59 sylan9eqr 
 |-  ( ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) /\ ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) -> ( ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) .x. ( n .^ X ) ) = ( 0g ` P ) )
61 32 60 syl5eq 
 |-  ( ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) /\ ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) -> [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( 0g ` P ) )
62 61 ex 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) -> [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( 0g ` P ) ) )
63 62 imim2d 
 |-  ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( ( s < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) -> ( s < n -> [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( 0g ` P ) ) ) )
64 63 ralimdva 
 |-  ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ s e. NN0 ) -> ( A. n e. NN0 ( s < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) -> A. n e. NN0 ( s < n -> [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( 0g ` P ) ) ) )
65 64 reximdva 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( E. s e. NN0 A. n e. NN0 ( s < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( 0g ` P ) ) ) )
66 13 65 mpd 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> E. s e. NN0 A. n e. NN0 ( s < n -> [_ n / k ]_ ( ( R gsum ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) ) .x. ( k .^ X ) ) = ( 0g ` P ) ) )
67 11 12 66 mptnn0fsupp 
 |-  ( ( 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 ) )