Metamath Proof Explorer

Theorem cply1mul

Description: The product of two constant polynomials is a constant polynomial. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cply1mul.p 
|- P = ( Poly1 ` R )
cply1mul.b 
|- B = ( Base ` P )
cply1mul.0 
|- .0. = ( 0g ` R )
cply1mul.m 
|- .X. = ( .r ` P )
Assertion cply1mul 
|- ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) -> A. c e. NN ( ( coe1 ` ( F .X. G ) ) ` c ) = .0. ) )

Proof

Step Hyp Ref Expression
1 cply1mul.p 
 |-  P = ( Poly1 ` R )
2 cply1mul.b 
 |-  B = ( Base ` P )
3 cply1mul.0 
 |-  .0. = ( 0g ` R )
4 cply1mul.m 
 |-  .X. = ( .r ` P )
5 eqid 
 |-  ( .r ` R ) = ( .r ` R )
6 1 4 5 2 coe1mul 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .X. G ) ) = ( s e. NN0 |-> ( R gsum ( k e. ( 0 ... s ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( s - k ) ) ) ) ) ) )
7 6 3expb 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( coe1 ` ( F .X. G ) ) = ( s e. NN0 |-> ( R gsum ( k e. ( 0 ... s ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( s - k ) ) ) ) ) ) )
8 7 adantr 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) -> ( coe1 ` ( F .X. G ) ) = ( s e. NN0 |-> ( R gsum ( k e. ( 0 ... s ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( s - k ) ) ) ) ) ) )
9 8 adantr 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) -> ( coe1 ` ( F .X. G ) ) = ( s e. NN0 |-> ( R gsum ( k e. ( 0 ... s ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( s - k ) ) ) ) ) ) )
10 oveq2 
 |-  ( s = n -> ( 0 ... s ) = ( 0 ... n ) )
11 fvoveq1 
 |-  ( s = n -> ( ( coe1 ` G ) ` ( s - k ) ) = ( ( coe1 ` G ) ` ( n - k ) ) )
12 11 oveq2d 
 |-  ( s = n -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( s - k ) ) ) = ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) )
13 10 12 mpteq12dv 
 |-  ( s = n -> ( k e. ( 0 ... s ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( s - k ) ) ) ) = ( k e. ( 0 ... n ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) ) )
14 13 oveq2d 
 |-  ( s = n -> ( R gsum ( k e. ( 0 ... s ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( s - k ) ) ) ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) ) ) )
15 14 adantl 
 |-  ( ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) /\ s = n ) -> ( R gsum ( k e. ( 0 ... s ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( s - k ) ) ) ) ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) ) ) )
16 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
17 16 adantl 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) -> n e. NN0 )
18 ovexd 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) -> ( R gsum ( k e. ( 0 ... n ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) ) ) e. _V )
19 9 15 17 18 fvmptd 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) -> ( ( coe1 ` ( F .X. G ) ) ` n ) = ( R gsum ( k e. ( 0 ... n ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) ) ) )
20 r19.26 
 |-  ( A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) <-> ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. /\ A. c e. NN ( ( coe1 ` G ) ` c ) = .0. ) )
21 oveq2 
 |-  ( k = 0 -> ( n - k ) = ( n - 0 ) )
22 nncn 
 |-  ( n e. NN -> n e. CC )
23 22 subid1d 
 |-  ( n e. NN -> ( n - 0 ) = n )
24 23 adantr 
 |-  ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( n - 0 ) = n )
25 21 24 sylan9eqr 
 |-  ( ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) -> ( n - k ) = n )
26 simpll 
 |-  ( ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) -> n e. NN )
27 25 26 eqeltrd 
 |-  ( ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) -> ( n - k ) e. NN )
28 fveqeq2 
 |-  ( c = ( n - k ) -> ( ( ( coe1 ` G ) ` c ) = .0. <-> ( ( coe1 ` G ) ` ( n - k ) ) = .0. ) )
29 28 rspcv 
 |-  ( ( n - k ) e. NN -> ( A. c e. NN ( ( coe1 ` G ) ` c ) = .0. -> ( ( coe1 ` G ) ` ( n - k ) ) = .0. ) )
30 27 29 syl 
 |-  ( ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) -> ( A. c e. NN ( ( coe1 ` G ) ` c ) = .0. -> ( ( coe1 ` G ) ` ( n - k ) ) = .0. ) )
31 oveq2 
 |-  ( ( ( coe1 ` G ) ` ( n - k ) ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = ( ( ( coe1 ` F ) ` k ) ( .r ` R ) .0. ) )
32 simpll 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) ) -> R e. Ring )
33 simprl 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> F e. B )
34 elfznn0 
 |-  ( k e. ( 0 ... n ) -> k e. NN0 )
35 34 adantl 
 |-  ( ( n e. NN /\ k e. ( 0 ... n ) ) -> k e. NN0 )
36 35 adantr 
 |-  ( ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) -> k e. NN0 )
37 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
38 eqid 
 |-  ( Base ` R ) = ( Base ` R )
39 37 2 1 38 coe1fvalcl 
 |-  ( ( F e. B /\ k e. NN0 ) -> ( ( coe1 ` F ) ` k ) e. ( Base ` R ) )
40 33 36 39 syl2an 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) ) -> ( ( coe1 ` F ) ` k ) e. ( Base ` R ) )
41 38 5 3 ringrz 
 |-  ( ( R e. Ring /\ ( ( coe1 ` F ) ` k ) e. ( Base ` R ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) .0. ) = .0. )
42 32 40 41 syl2anc 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) .0. ) = .0. )
43 31 42 sylan9eqr 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) ) /\ ( ( coe1 ` G ) ` ( n - k ) ) = .0. ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. )
44 43 ex 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) ) -> ( ( ( coe1 ` G ) ` ( n - k ) ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) )
45 44 expcom 
 |-  ( ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` G ) ` ( n - k ) ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) )
46 45 com23 
 |-  ( ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) -> ( ( ( coe1 ` G ) ` ( n - k ) ) = .0. -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) )
47 30 46 syldc 
 |-  ( A. c e. NN ( ( coe1 ` G ) ` c ) = .0. -> ( ( ( n e. NN /\ k e. ( 0 ... n ) ) /\ k = 0 ) -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) )
48 47 expd 
 |-  ( A. c e. NN ( ( coe1 ` G ) ` c ) = .0. -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( k = 0 -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
49 48 com24 
 |-  ( A. c e. NN ( ( coe1 ` G ) ` c ) = .0. -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( k = 0 -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
50 49 adantl 
 |-  ( ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. /\ A. c e. NN ( ( coe1 ` G ) ` c ) = .0. ) -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( k = 0 -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
51 50 com13 
 |-  ( k = 0 -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. /\ A. c e. NN ( ( coe1 ` G ) ` c ) = .0. ) -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
52 neqne 
 |-  ( -. k = 0 -> k =/= 0 )
53 52 34 anim12ci 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... n ) ) -> ( k e. NN0 /\ k =/= 0 ) )
54 elnnne0 
 |-  ( k e. NN <-> ( k e. NN0 /\ k =/= 0 ) )
55 53 54 sylibr 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... n ) ) -> k e. NN )
56 fveqeq2 
 |-  ( c = k -> ( ( ( coe1 ` F ) ` c ) = .0. <-> ( ( coe1 ` F ) ` k ) = .0. ) )
57 56 rspcv 
 |-  ( k e. NN -> ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. -> ( ( coe1 ` F ) ` k ) = .0. ) )
58 55 57 syl 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... n ) ) -> ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. -> ( ( coe1 ` F ) ` k ) = .0. ) )
59 oveq1 
 |-  ( ( ( coe1 ` F ) ` k ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = ( .0. ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) )
60 simpll 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ k e. ( 0 ... n ) ) -> R e. Ring )
61 2 eleq2i 
 |-  ( G e. B <-> G e. ( Base ` P ) )
62 61 biimpi 
 |-  ( G e. B -> G e. ( Base ` P ) )
63 62 adantl 
 |-  ( ( F e. B /\ G e. B ) -> G e. ( Base ` P ) )
64 63 adantl 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> G e. ( Base ` P ) )
65 fznn0sub 
 |-  ( k e. ( 0 ... n ) -> ( n - k ) e. NN0 )
66 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
67 eqid 
 |-  ( Base ` P ) = ( Base ` P )
68 66 67 1 38 coe1fvalcl 
 |-  ( ( G e. ( Base ` P ) /\ ( n - k ) e. NN0 ) -> ( ( coe1 ` G ) ` ( n - k ) ) e. ( Base ` R ) )
69 64 65 68 syl2an 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ k e. ( 0 ... n ) ) -> ( ( coe1 ` G ) ` ( n - k ) ) e. ( Base ` R ) )
70 38 5 3 ringlz 
 |-  ( ( R e. Ring /\ ( ( coe1 ` G ) ` ( n - k ) ) e. ( Base ` R ) ) -> ( .0. ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. )
71 60 69 70 syl2anc 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ k e. ( 0 ... n ) ) -> ( .0. ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. )
72 59 71 sylan9eqr 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ k e. ( 0 ... n ) ) /\ ( ( coe1 ` F ) ` k ) = .0. ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. )
73 72 ex 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) )
74 73 ex 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( k e. ( 0 ... n ) -> ( ( ( coe1 ` F ) ` k ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) )
75 74 com23 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` F ) ` k ) = .0. -> ( k e. ( 0 ... n ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) )
76 75 a1dd 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` F ) ` k ) = .0. -> ( n e. NN -> ( k e. ( 0 ... n ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
77 76 com14 
 |-  ( k e. ( 0 ... n ) -> ( ( ( coe1 ` F ) ` k ) = .0. -> ( n e. NN -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
78 77 adantl 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) = .0. -> ( n e. NN -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
79 58 78 syld 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... n ) ) -> ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. -> ( n e. NN -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
80 79 com24 
 |-  ( ( -. k = 0 /\ k e. ( 0 ... n ) ) -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( n e. NN -> ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
81 80 ex 
 |-  ( -. k = 0 -> ( k e. ( 0 ... n ) -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( n e. NN -> ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) ) )
82 81 com14 
 |-  ( n e. NN -> ( k e. ( 0 ... n ) -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( -. k = 0 -> ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) ) )
83 82 imp 
 |-  ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( -. k = 0 -> ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
84 83 com14 
 |-  ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( -. k = 0 -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
85 84 adantr 
 |-  ( ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. /\ A. c e. NN ( ( coe1 ` G ) ` c ) = .0. ) -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( -. k = 0 -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
86 85 com13 
 |-  ( -. k = 0 -> ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. /\ A. c e. NN ( ( coe1 ` G ) ` c ) = .0. ) -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) ) )
87 51 86 pm2.61i 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( ( A. c e. NN ( ( coe1 ` F ) ` c ) = .0. /\ A. c e. NN ( ( coe1 ` G ) ` c ) = .0. ) -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) )
88 20 87 biimtrid 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) ) )
89 88 imp 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) -> ( ( n e. NN /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. ) )
90 89 impl 
 |-  ( ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) /\ k e. ( 0 ... n ) ) -> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) = .0. )
91 90 mpteq2dva 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) -> ( k e. ( 0 ... n ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) ) = ( k e. ( 0 ... n ) |-> .0. ) )
92 91 oveq2d 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) -> ( R gsum ( k e. ( 0 ... n ) |-> ( ( ( coe1 ` F ) ` k ) ( .r ` R ) ( ( coe1 ` G ) ` ( n - k ) ) ) ) ) = ( R gsum ( k e. ( 0 ... n ) |-> .0. ) ) )
93 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
94 ovexd 
 |-  ( R e. Ring -> ( 0 ... n ) e. _V )
95 3 gsumz 
 |-  ( ( R e. Mnd /\ ( 0 ... n ) e. _V ) -> ( R gsum ( k e. ( 0 ... n ) |-> .0. ) ) = .0. )
96 93 94 95 syl2anc 
 |-  ( R e. Ring -> ( R gsum ( k e. ( 0 ... n ) |-> .0. ) ) = .0. )
97 96 adantr 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( R gsum ( k e. ( 0 ... n ) |-> .0. ) ) = .0. )
98 97 adantr 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) -> ( R gsum ( k e. ( 0 ... n ) |-> .0. ) ) = .0. )
99 98 adantr 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) -> ( R gsum ( k e. ( 0 ... n ) |-> .0. ) ) = .0. )
100 19 92 99 3eqtrd 
 |-  ( ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) /\ n e. NN ) -> ( ( coe1 ` ( F .X. G ) ) ` n ) = .0. )
101 100 ralrimiva 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) -> A. n e. NN ( ( coe1 ` ( F .X. G ) ) ` n ) = .0. )
102 fveqeq2 
 |-  ( c = n -> ( ( ( coe1 ` ( F .X. G ) ) ` c ) = .0. <-> ( ( coe1 ` ( F .X. G ) ) ` n ) = .0. ) )
103 102 cbvralvw 
 |-  ( A. c e. NN ( ( coe1 ` ( F .X. G ) ) ` c ) = .0. <-> A. n e. NN ( ( coe1 ` ( F .X. G ) ) ` n ) = .0. )
104 101 103 sylibr 
 |-  ( ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) /\ A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) ) -> A. c e. NN ( ( coe1 ` ( F .X. G ) ) ` c ) = .0. )
105 104 ex 
 |-  ( ( R e. Ring /\ ( F e. B /\ G e. B ) ) -> ( A. c e. NN ( ( ( coe1 ` F ) ` c ) = .0. /\ ( ( coe1 ` G ) ` c ) = .0. ) -> A. c e. NN ( ( coe1 ` ( F .X. G ) ) ` c ) = .0. ) )