Metamath Proof Explorer

Theorem ply1mulgsumlem2

Description: Lemma 2 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 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 ) ) )

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 2 3 4 5 6 7 8 9 10 ply1mulgsumlem1 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> E. z e. NN0 A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) )
12 2nn0 
 |-  2 e. NN0
13 12 a1i 
 |-  ( z e. NN0 -> 2 e. NN0 )
14 id 
 |-  ( z e. NN0 -> z e. NN0 )
15 13 14 nn0mulcld 
 |-  ( z e. NN0 -> ( 2 x. z ) e. NN0 )
16 15 ad2antrr 
 |-  ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) -> ( 2 x. z ) e. NN0 )
17 breq1 
 |-  ( s = ( 2 x. z ) -> ( s < n <-> ( 2 x. z ) < n ) )
18 17 imbi1d 
 |-  ( s = ( 2 x. z ) -> ( ( s < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) <-> ( ( 2 x. z ) < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) ) )
19 18 ralbidv 
 |-  ( s = ( 2 x. z ) -> ( A. n e. NN0 ( s < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) <-> A. n e. NN0 ( ( 2 x. z ) < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) ) )
20 19 adantl 
 |-  ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ s = ( 2 x. z ) ) -> ( A. n e. NN0 ( s < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) <-> A. n e. NN0 ( ( 2 x. z ) < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) ) )
21 2re 
 |-  2 e. RR
22 21 a1i 
 |-  ( z e. NN0 -> 2 e. RR )
23 nn0re 
 |-  ( z e. NN0 -> z e. RR )
24 22 23 remulcld 
 |-  ( z e. NN0 -> ( 2 x. z ) e. RR )
25 24 ad2antrr 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( 2 x. z ) e. RR )
26 nn0re 
 |-  ( n e. NN0 -> n e. RR )
27 26 adantl 
 |-  ( ( z e. NN0 /\ n e. NN0 ) -> n e. RR )
28 27 adantr 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> n e. RR )
29 elfznn0 
 |-  ( l e. ( 0 ... n ) -> l e. NN0 )
30 nn0re 
 |-  ( l e. NN0 -> l e. RR )
31 29 30 syl 
 |-  ( l e. ( 0 ... n ) -> l e. RR )
32 31 adantl 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> l e. RR )
33 25 28 32 ltsub1d 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( 2 x. z ) < n <-> ( ( 2 x. z ) - l ) < ( n - l ) ) )
34 23 ad2antrr 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> z e. RR )
35 32 34 25 lesub2d 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( l <_ z <-> ( ( 2 x. z ) - z ) <_ ( ( 2 x. z ) - l ) ) )
36 35 adantr 
 |-  ( ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ ( ( 2 x. z ) - l ) < ( n - l ) ) -> ( l <_ z <-> ( ( 2 x. z ) - z ) <_ ( ( 2 x. z ) - l ) ) )
37 24 23 resubcld 
 |-  ( z e. NN0 -> ( ( 2 x. z ) - z ) e. RR )
38 37 ad2antrr 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( 2 x. z ) - z ) e. RR )
39 24 adantr 
 |-  ( ( z e. NN0 /\ n e. NN0 ) -> ( 2 x. z ) e. RR )
40 resubcl 
 |-  ( ( ( 2 x. z ) e. RR /\ l e. RR ) -> ( ( 2 x. z ) - l ) e. RR )
41 39 31 40 syl2an 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( 2 x. z ) - l ) e. RR )
42 resubcl 
 |-  ( ( n e. RR /\ l e. RR ) -> ( n - l ) e. RR )
43 27 31 42 syl2an 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( n - l ) e. RR )
44 lelttr 
 |-  ( ( ( ( 2 x. z ) - z ) e. RR /\ ( ( 2 x. z ) - l ) e. RR /\ ( n - l ) e. RR ) -> ( ( ( ( 2 x. z ) - z ) <_ ( ( 2 x. z ) - l ) /\ ( ( 2 x. z ) - l ) < ( n - l ) ) -> ( ( 2 x. z ) - z ) < ( n - l ) ) )
45 38 41 43 44 syl3anc 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( ( ( 2 x. z ) - z ) <_ ( ( 2 x. z ) - l ) /\ ( ( 2 x. z ) - l ) < ( n - l ) ) -> ( ( 2 x. z ) - z ) < ( n - l ) ) )
46 nn0cn 
 |-  ( z e. NN0 -> z e. CC )
47 2txmxeqx 
 |-  ( z e. CC -> ( ( 2 x. z ) - z ) = z )
48 46 47 syl 
 |-  ( z e. NN0 -> ( ( 2 x. z ) - z ) = z )
49 48 ad2antrr 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( 2 x. z ) - z ) = z )
50 49 breq1d 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( ( 2 x. z ) - z ) < ( n - l ) <-> z < ( n - l ) ) )
51 45 50 sylibd 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( ( ( 2 x. z ) - z ) <_ ( ( 2 x. z ) - l ) /\ ( ( 2 x. z ) - l ) < ( n - l ) ) -> z < ( n - l ) ) )
52 51 expcomd 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( ( 2 x. z ) - l ) < ( n - l ) -> ( ( ( 2 x. z ) - z ) <_ ( ( 2 x. z ) - l ) -> z < ( n - l ) ) ) )
53 52 imp 
 |-  ( ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ ( ( 2 x. z ) - l ) < ( n - l ) ) -> ( ( ( 2 x. z ) - z ) <_ ( ( 2 x. z ) - l ) -> z < ( n - l ) ) )
54 36 53 sylbid 
 |-  ( ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) /\ ( ( 2 x. z ) - l ) < ( n - l ) ) -> ( l <_ z -> z < ( n - l ) ) )
55 54 ex 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( ( 2 x. z ) - l ) < ( n - l ) -> ( l <_ z -> z < ( n - l ) ) ) )
56 33 55 sylbid 
 |-  ( ( ( z e. NN0 /\ n e. NN0 ) /\ l e. ( 0 ... n ) ) -> ( ( 2 x. z ) < n -> ( l <_ z -> z < ( n - l ) ) ) )
57 56 ex 
 |-  ( ( z e. NN0 /\ n e. NN0 ) -> ( l e. ( 0 ... n ) -> ( ( 2 x. z ) < n -> ( l <_ z -> z < ( n - l ) ) ) ) )
58 57 com23 
 |-  ( ( z e. NN0 /\ n e. NN0 ) -> ( ( 2 x. z ) < n -> ( l e. ( 0 ... n ) -> ( l <_ z -> z < ( n - l ) ) ) ) )
59 58 ex 
 |-  ( z e. NN0 -> ( n e. NN0 -> ( ( 2 x. z ) < n -> ( l e. ( 0 ... n ) -> ( l <_ z -> z < ( n - l ) ) ) ) ) )
60 59 ad2antrr 
 |-  ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) -> ( n e. NN0 -> ( ( 2 x. z ) < n -> ( l e. ( 0 ... n ) -> ( l <_ z -> z < ( n - l ) ) ) ) ) )
61 60 imp41 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> ( l <_ z -> z < ( n - l ) ) )
62 61 impcom 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> z < ( n - l ) )
63 fznn0sub2 
 |-  ( l e. ( 0 ... n ) -> ( n - l ) e. ( 0 ... n ) )
64 elfznn0 
 |-  ( ( n - l ) e. ( 0 ... n ) -> ( n - l ) e. NN0 )
65 breq2 
 |-  ( x = ( n - l ) -> ( z < x <-> z < ( n - l ) ) )
66 fveqeq2 
 |-  ( x = ( n - l ) -> ( ( A ` x ) = ( 0g ` R ) <-> ( A ` ( n - l ) ) = ( 0g ` R ) ) )
67 fveqeq2 
 |-  ( x = ( n - l ) -> ( ( C ` x ) = ( 0g ` R ) <-> ( C ` ( n - l ) ) = ( 0g ` R ) ) )
68 66 67 anbi12d 
 |-  ( x = ( n - l ) -> ( ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) <-> ( ( A ` ( n - l ) ) = ( 0g ` R ) /\ ( C ` ( n - l ) ) = ( 0g ` R ) ) ) )
69 65 68 imbi12d 
 |-  ( x = ( n - l ) -> ( ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) <-> ( z < ( n - l ) -> ( ( A ` ( n - l ) ) = ( 0g ` R ) /\ ( C ` ( n - l ) ) = ( 0g ` R ) ) ) ) )
70 69 rspcva 
 |-  ( ( ( n - l ) e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) -> ( z < ( n - l ) -> ( ( A ` ( n - l ) ) = ( 0g ` R ) /\ ( C ` ( n - l ) ) = ( 0g ` R ) ) ) )
71 simpr 
 |-  ( ( ( A ` ( n - l ) ) = ( 0g ` R ) /\ ( C ` ( n - l ) ) = ( 0g ` R ) ) -> ( C ` ( n - l ) ) = ( 0g ` R ) )
72 70 71 syl6 
 |-  ( ( ( n - l ) e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) -> ( z < ( n - l ) -> ( C ` ( n - l ) ) = ( 0g ` R ) ) )
73 72 ex 
 |-  ( ( n - l ) e. NN0 -> ( A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) -> ( z < ( n - l ) -> ( C ` ( n - l ) ) = ( 0g ` R ) ) ) )
74 63 64 73 3syl 
 |-  ( l e. ( 0 ... n ) -> ( A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) -> ( z < ( n - l ) -> ( C ` ( n - l ) ) = ( 0g ` R ) ) ) )
75 74 com12 
 |-  ( A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) -> ( l e. ( 0 ... n ) -> ( z < ( n - l ) -> ( C ` ( n - l ) ) = ( 0g ` R ) ) ) )
76 75 ad4antlr 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> ( l e. ( 0 ... n ) -> ( z < ( n - l ) -> ( C ` ( n - l ) ) = ( 0g ` R ) ) ) )
77 76 imp 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> ( z < ( n - l ) -> ( C ` ( n - l ) ) = ( 0g ` R ) ) )
78 77 adantl 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( z < ( n - l ) -> ( C ` ( n - l ) ) = ( 0g ` R ) ) )
79 62 78 mpd 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( C ` ( n - l ) ) = ( 0g ` R ) )
80 79 oveq2d 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( ( A ` l ) .* ( C ` ( n - l ) ) ) = ( ( A ` l ) .* ( 0g ` R ) ) )
81 simplr1 
 |-  ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> R e. Ring )
82 81 ad2antrr 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> R e. Ring )
83 82 adantl 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> R e. Ring )
84 simplr2 
 |-  ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> K e. B )
85 84 adantr 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> K e. B )
86 85 29 anim12i 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> ( K e. B /\ l e. NN0 ) )
87 86 adantl 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( K e. B /\ l e. NN0 ) )
88 eqid 
 |-  ( Base ` R ) = ( Base ` R )
89 3 2 1 88 coe1fvalcl 
 |-  ( ( K e. B /\ l e. NN0 ) -> ( A ` l ) e. ( Base ` R ) )
90 87 89 syl 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( A ` l ) e. ( Base ` R ) )
91 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
92 88 8 91 ringrz 
 |-  ( ( R e. Ring /\ ( A ` l ) e. ( Base ` R ) ) -> ( ( A ` l ) .* ( 0g ` R ) ) = ( 0g ` R ) )
93 83 90 92 syl2anc 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( ( A ` l ) .* ( 0g ` R ) ) = ( 0g ` R ) )
94 80 93 eqtrd 
 |-  ( ( l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( ( A ` l ) .* ( C ` ( n - l ) ) ) = ( 0g ` R ) )
95 ltnle 
 |-  ( ( z e. RR /\ l e. RR ) -> ( z < l <-> -. l <_ z ) )
96 23 30 95 syl2an 
 |-  ( ( z e. NN0 /\ l e. NN0 ) -> ( z < l <-> -. l <_ z ) )
97 96 bicomd 
 |-  ( ( z e. NN0 /\ l e. NN0 ) -> ( -. l <_ z <-> z < l ) )
98 97 expcom 
 |-  ( l e. NN0 -> ( z e. NN0 -> ( -. l <_ z <-> z < l ) ) )
99 98 29 syl11 
 |-  ( z e. NN0 -> ( l e. ( 0 ... n ) -> ( -. l <_ z <-> z < l ) ) )
100 99 ad4antr 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> ( l e. ( 0 ... n ) -> ( -. l <_ z <-> z < l ) ) )
101 100 imp 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> ( -. l <_ z <-> z < l ) )
102 breq2 
 |-  ( x = l -> ( z < x <-> z < l ) )
103 fveqeq2 
 |-  ( x = l -> ( ( A ` x ) = ( 0g ` R ) <-> ( A ` l ) = ( 0g ` R ) ) )
104 fveqeq2 
 |-  ( x = l -> ( ( C ` x ) = ( 0g ` R ) <-> ( C ` l ) = ( 0g ` R ) ) )
105 103 104 anbi12d 
 |-  ( x = l -> ( ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) <-> ( ( A ` l ) = ( 0g ` R ) /\ ( C ` l ) = ( 0g ` R ) ) ) )
106 102 105 imbi12d 
 |-  ( x = l -> ( ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) <-> ( z < l -> ( ( A ` l ) = ( 0g ` R ) /\ ( C ` l ) = ( 0g ` R ) ) ) ) )
107 106 rspcva 
 |-  ( ( l e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) -> ( z < l -> ( ( A ` l ) = ( 0g ` R ) /\ ( C ` l ) = ( 0g ` R ) ) ) )
108 simpl 
 |-  ( ( ( A ` l ) = ( 0g ` R ) /\ ( C ` l ) = ( 0g ` R ) ) -> ( A ` l ) = ( 0g ` R ) )
109 107 108 syl6 
 |-  ( ( l e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) -> ( z < l -> ( A ` l ) = ( 0g ` R ) ) )
110 109 ex 
 |-  ( l e. NN0 -> ( A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) -> ( z < l -> ( A ` l ) = ( 0g ` R ) ) ) )
111 110 29 syl11 
 |-  ( A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) -> ( l e. ( 0 ... n ) -> ( z < l -> ( A ` l ) = ( 0g ` R ) ) ) )
112 111 ad4antlr 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> ( l e. ( 0 ... n ) -> ( z < l -> ( A ` l ) = ( 0g ` R ) ) ) )
113 112 imp 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> ( z < l -> ( A ` l ) = ( 0g ` R ) ) )
114 101 113 sylbid 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> ( -. l <_ z -> ( A ` l ) = ( 0g ` R ) ) )
115 114 impcom 
 |-  ( ( -. l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( A ` l ) = ( 0g ` R ) )
116 115 oveq1d 
 |-  ( ( -. l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( ( A ` l ) .* ( C ` ( n - l ) ) ) = ( ( 0g ` R ) .* ( C ` ( n - l ) ) ) )
117 82 adantl 
 |-  ( ( -. l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> R e. Ring )
118 simplr3 
 |-  ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> L e. B )
119 118 adantr 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> L e. B )
120 fznn0sub 
 |-  ( l e. ( 0 ... n ) -> ( n - l ) e. NN0 )
121 119 120 anim12i 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> ( L e. B /\ ( n - l ) e. NN0 ) )
122 121 adantl 
 |-  ( ( -. l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( L e. B /\ ( n - l ) e. NN0 ) )
123 4 2 1 88 coe1fvalcl 
 |-  ( ( L e. B /\ ( n - l ) e. NN0 ) -> ( C ` ( n - l ) ) e. ( Base ` R ) )
124 122 123 syl 
 |-  ( ( -. l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( C ` ( n - l ) ) e. ( Base ` R ) )
125 88 8 91 ringlz 
 |-  ( ( R e. Ring /\ ( C ` ( n - l ) ) e. ( Base ` R ) ) -> ( ( 0g ` R ) .* ( C ` ( n - l ) ) ) = ( 0g ` R ) )
126 117 124 125 syl2anc 
 |-  ( ( -. l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( ( 0g ` R ) .* ( C ` ( n - l ) ) ) = ( 0g ` R ) )
127 116 126 eqtrd 
 |-  ( ( -. l <_ z /\ ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) ) -> ( ( A ` l ) .* ( C ` ( n - l ) ) ) = ( 0g ` R ) )
128 94 127 pm2.61ian 
 |-  ( ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) /\ l e. ( 0 ... n ) ) -> ( ( A ` l ) .* ( C ` ( n - l ) ) ) = ( 0g ` R ) )
129 128 mpteq2dva 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) = ( l e. ( 0 ... n ) |-> ( 0g ` R ) ) )
130 129 oveq2d 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( R gsum ( l e. ( 0 ... n ) |-> ( 0g ` R ) ) ) )
131 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
132 131 3ad2ant1 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> R e. Mnd )
133 ovex 
 |-  ( 0 ... n ) e. _V
134 132 133 jctir 
 |-  ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( R e. Mnd /\ ( 0 ... n ) e. _V ) )
135 134 ad3antlr 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> ( R e. Mnd /\ ( 0 ... n ) e. _V ) )
136 91 gsumz 
 |-  ( ( R e. Mnd /\ ( 0 ... n ) e. _V ) -> ( R gsum ( l e. ( 0 ... n ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
137 135 136 syl 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> ( R gsum ( l e. ( 0 ... n ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
138 130 137 eqtrd 
 |-  ( ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( 2 x. z ) < n ) -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) )
139 138 ex 
 |-  ( ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( 2 x. z ) < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) )
140 139 ralrimiva 
 |-  ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) -> A. n e. NN0 ( ( 2 x. z ) < n -> ( R gsum ( l e. ( 0 ... n ) |-> ( ( A ` l ) .* ( C ` ( n - l ) ) ) ) ) = ( 0g ` R ) ) )
141 16 20 140 rspcedvd 
 |-  ( ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) /\ ( 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 ) ) )
142 141 ex 
 |-  ( ( z e. NN0 /\ A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) ) -> ( ( 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 ) ) ) )
143 142 rexlimiva 
 |-  ( E. z e. NN0 A. x e. NN0 ( z < x -> ( ( A ` x ) = ( 0g ` R ) /\ ( C ` x ) = ( 0g ` R ) ) ) -> ( ( 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 ) ) ) )
144 11 143 mpcom 
 |-  ( ( 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 ) ) )