Metamath Proof Explorer

Theorem ply1mulgsumlem3

Description: Lemma 3 for ply1mulgsum . (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 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 ) )

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 ` R ) 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 ) ) ) ) ) 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 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 ) ) ) ) ) )
16 id 
 |-  ( n e. _V -> n e. _V )
17 oveq2 
 |-  ( k = n -> ( 0 ... k ) = ( 0 ... n ) )
18 fvoveq1 
 |-  ( k = n -> ( C ` ( k - l ) ) = ( C ` ( n - l ) ) )
19 18 oveq2d 
 |-  ( k = n -> ( ( A ` l ) .* ( C ` ( k - l ) ) ) = ( ( A ` l ) .* ( C ` ( n - l ) ) ) )
20 17 19 mpteq12dv 
 |-  ( k = n -> ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
21 20 adantl 
 |-  ( ( n e. _V /\ k = n ) -> ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
22 16 21 csbied 
 |-  ( n e. _V -> [_ n / k ]_ ( l e. ( 0 ... k ) |-> ( ( A ` l ) .* ( C ` ( k - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) )
23 22 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 ) ) ) ) ) )
24 15 23 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 ) ) ) ) ) )
25 14 24 ax-mp 
 |-  [_ 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 simpr 
 |-  ( ( ( ( ( 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 ) ) ) ) ) = ( 0g ` R ) )
27 25 26 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 ) ) ) ) ) = ( 0g ` R ) )
28 27 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 ) ) ) ) ) = ( 0g ` R ) ) )
29 28 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 ) ) ) ) ) = ( 0g ` R ) ) ) )
30 29 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 ) ) ) ) ) = ( 0g ` R ) ) ) )
31 30 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 ) ) ) ) ) = ( 0g ` R ) ) ) )
32 13 31 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 ) ) ) ) ) = ( 0g ` R ) ) )
33 11 12 32 mptnn0fsupp 
 |-  ( ( 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 ) )