Metamath Proof Explorer

Theorem coe1mul2

Description: The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1mul2.s 
|- S = ( PwSer1 ` R )
coe1mul2.t 
|- .xb = ( .r ` S )
coe1mul2.u 
|- .x. = ( .r ` R )
coe1mul2.b 
|- B = ( Base ` S )
Assertion coe1mul2 
|- ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsum ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 coe1mul2.s 
 |-  S = ( PwSer1 ` R )
2 coe1mul2.t 
 |-  .xb = ( .r ` S )
3 coe1mul2.u 
 |-  .x. = ( .r ` R )
4 coe1mul2.b 
 |-  B = ( Base ` S )
5 fconst6g 
 |-  ( k e. NN0 -> ( 1o X. { k } ) : 1o --> NN0 )
6 nn0ex 
 |-  NN0 e. _V
7 1on 
 |-  1o e. On
8 7 elexi 
 |-  1o e. _V
9 6 8 elmap 
 |-  ( ( 1o X. { k } ) e. ( NN0 ^m 1o ) <-> ( 1o X. { k } ) : 1o --> NN0 )
10 5 9 sylibr 
 |-  ( k e. NN0 -> ( 1o X. { k } ) e. ( NN0 ^m 1o ) )
11 10 adantl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( 1o X. { k } ) e. ( NN0 ^m 1o ) )
12 eqidd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( k e. NN0 |-> ( 1o X. { k } ) ) = ( k e. NN0 |-> ( 1o X. { k } ) ) )
13 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
14 1 4 13 psr1bas2 
 |-  B = ( Base ` ( 1o mPwSer R ) )
15 1 13 2 psr1mulr 
 |-  .xb = ( .r ` ( 1o mPwSer R ) )
16 psr1baslem 
 |-  ( NN0 ^m 1o ) = { a e. ( NN0 ^m 1o ) | ( `' a " NN ) e. Fin }
17 simp2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> F e. B )
18 simp3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> G e. B )
19 13 14 3 15 16 17 18 psrmulfval 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) = ( b e. ( NN0 ^m 1o ) |-> ( R gsum ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ b } |-> ( ( F ` c ) .x. ( G ` ( b oF - c ) ) ) ) ) ) )
20 breq2 
 |-  ( b = ( 1o X. { k } ) -> ( d oR <_ b <-> d oR <_ ( 1o X. { k } ) ) )
21 20 rabbidv 
 |-  ( b = ( 1o X. { k } ) -> { d e. ( NN0 ^m 1o ) | d oR <_ b } = { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } )
22 fvoveq1 
 |-  ( b = ( 1o X. { k } ) -> ( G ` ( b oF - c ) ) = ( G ` ( ( 1o X. { k } ) oF - c ) ) )
23 22 oveq2d 
 |-  ( b = ( 1o X. { k } ) -> ( ( F ` c ) .x. ( G ` ( b oF - c ) ) ) = ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) )
24 21 23 mpteq12dv 
 |-  ( b = ( 1o X. { k } ) -> ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ b } |-> ( ( F ` c ) .x. ( G ` ( b oF - c ) ) ) ) = ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) ) )
25 24 oveq2d 
 |-  ( b = ( 1o X. { k } ) -> ( R gsum ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ b } |-> ( ( F ` c ) .x. ( G ` ( b oF - c ) ) ) ) ) = ( R gsum ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) ) ) )
26 11 12 19 25 fmptco 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( ( F .xb G ) o. ( k e. NN0 |-> ( 1o X. { k } ) ) ) = ( k e. NN0 |-> ( R gsum ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) ) ) ) )
27 1 psr1ring 
 |-  ( R e. Ring -> S e. Ring )
28 4 2 ringcl 
 |-  ( ( S e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) e. B )
29 27 28 syl3an1 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .xb G ) e. B )
30 eqid 
 |-  ( coe1 ` ( F .xb G ) ) = ( coe1 ` ( F .xb G ) )
31 eqid 
 |-  ( k e. NN0 |-> ( 1o X. { k } ) ) = ( k e. NN0 |-> ( 1o X. { k } ) )
32 30 4 1 31 coe1fval3 
 |-  ( ( F .xb G ) e. B -> ( coe1 ` ( F .xb G ) ) = ( ( F .xb G ) o. ( k e. NN0 |-> ( 1o X. { k } ) ) ) )
33 29 32 syl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .xb G ) ) = ( ( F .xb G ) o. ( k e. NN0 |-> ( 1o X. { k } ) ) ) )
34 eqid 
 |-  ( Base ` R ) = ( Base ` R )
35 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
36 simpl1 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> R e. Ring )
37 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
38 36 37 syl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> R e. CMnd )
39 fzfi 
 |-  ( 0 ... k ) e. Fin
40 39 a1i 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( 0 ... k ) e. Fin )
41 simpll1 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> R e. Ring )
42 simpll2 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> F e. B )
43 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
44 43 4 1 34 coe1f2 
 |-  ( F e. B -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
45 42 44 syl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
46 elfznn0 
 |-  ( x e. ( 0 ... k ) -> x e. NN0 )
47 46 adantl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> x e. NN0 )
48 45 47 ffvelcdmd 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> ( ( coe1 ` F ) ` x ) e. ( Base ` R ) )
49 simpll3 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> G e. B )
50 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
51 50 4 1 34 coe1f2 
 |-  ( G e. B -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
52 49 51 syl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
53 fznn0sub 
 |-  ( x e. ( 0 ... k ) -> ( k - x ) e. NN0 )
54 53 adantl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> ( k - x ) e. NN0 )
55 52 54 ffvelcdmd 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> ( ( coe1 ` G ) ` ( k - x ) ) e. ( Base ` R ) )
56 34 3 ringcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` F ) ` x ) e. ( Base ` R ) /\ ( ( coe1 ` G ) ` ( k - x ) ) e. ( Base ` R ) ) -> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) e. ( Base ` R ) )
57 41 48 55 56 syl3anc 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ x e. ( 0 ... k ) ) -> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) e. ( Base ` R ) )
58 57 fmpttd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) : ( 0 ... k ) --> ( Base ` R ) )
59 39 elexi 
 |-  ( 0 ... k ) e. _V
60 59 mptex 
 |-  ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) e. _V
61 funmpt 
 |-  Fun ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) )
62 fvex 
 |-  ( 0g ` R ) e. _V
63 60 61 62 3pm3.2i 
 |-  ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) e. _V /\ Fun ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) /\ ( 0g ` R ) e. _V )
64 suppssdm 
 |-  ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) supp ( 0g ` R ) ) C_ dom ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) )
65 eqid 
 |-  ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) = ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) )
66 65 dmmptss 
 |-  dom ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) C_ ( 0 ... k )
67 64 66 sstri 
 |-  ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) supp ( 0g ` R ) ) C_ ( 0 ... k )
68 39 67 pm3.2i 
 |-  ( ( 0 ... k ) e. Fin /\ ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) supp ( 0g ` R ) ) C_ ( 0 ... k ) )
69 suppssfifsupp 
 |-  ( ( ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) e. _V /\ Fun ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) /\ ( 0g ` R ) e. _V ) /\ ( ( 0 ... k ) e. Fin /\ ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) supp ( 0g ` R ) ) C_ ( 0 ... k ) ) ) -> ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) finSupp ( 0g ` R ) )
70 63 68 69 mp2an 
 |-  ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) finSupp ( 0g ` R )
71 70 a1i 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) finSupp ( 0g ` R ) )
72 eqid 
 |-  { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } = { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) }
73 72 coe1mul2lem2 
 |-  ( k e. NN0 -> ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( c ` (/) ) ) : { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } -1-1-onto-> ( 0 ... k ) )
74 73 adantl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( c ` (/) ) ) : { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } -1-1-onto-> ( 0 ... k ) )
75 34 35 38 40 58 71 74 gsumf1o 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( R gsum ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) ) = ( R gsum ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) o. ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( c ` (/) ) ) ) ) )
76 breq1 
 |-  ( d = c -> ( d oR <_ ( 1o X. { k } ) <-> c oR <_ ( 1o X. { k } ) ) )
77 76 elrab 
 |-  ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } <-> ( c e. ( NN0 ^m 1o ) /\ c oR <_ ( 1o X. { k } ) ) )
78 77 simprbi 
 |-  ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } -> c oR <_ ( 1o X. { k } ) )
79 78 adantl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> c oR <_ ( 1o X. { k } ) )
80 simplr 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> k e. NN0 )
81 elrabi 
 |-  ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } -> c e. ( NN0 ^m 1o ) )
82 81 adantl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> c e. ( NN0 ^m 1o ) )
83 coe1mul2lem1 
 |-  ( ( k e. NN0 /\ c e. ( NN0 ^m 1o ) ) -> ( c oR <_ ( 1o X. { k } ) <-> ( c ` (/) ) e. ( 0 ... k ) ) )
84 80 82 83 syl2anc 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( c oR <_ ( 1o X. { k } ) <-> ( c ` (/) ) e. ( 0 ... k ) ) )
85 79 84 mpbid 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( c ` (/) ) e. ( 0 ... k ) )
86 eqidd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( c ` (/) ) ) = ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( c ` (/) ) ) )
87 eqidd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) = ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) )
88 fveq2 
 |-  ( x = ( c ` (/) ) -> ( ( coe1 ` F ) ` x ) = ( ( coe1 ` F ) ` ( c ` (/) ) ) )
89 oveq2 
 |-  ( x = ( c ` (/) ) -> ( k - x ) = ( k - ( c ` (/) ) ) )
90 89 fveq2d 
 |-  ( x = ( c ` (/) ) -> ( ( coe1 ` G ) ` ( k - x ) ) = ( ( coe1 ` G ) ` ( k - ( c ` (/) ) ) ) )
91 88 90 oveq12d 
 |-  ( x = ( c ` (/) ) -> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) = ( ( ( coe1 ` F ) ` ( c ` (/) ) ) .x. ( ( coe1 ` G ) ` ( k - ( c ` (/) ) ) ) ) )
92 85 86 87 91 fmptco 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) o. ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( c ` (/) ) ) ) = ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( ( coe1 ` F ) ` ( c ` (/) ) ) .x. ( ( coe1 ` G ) ` ( k - ( c ` (/) ) ) ) ) ) )
93 simpll2 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> F e. B )
94 43 fvcoe1 
 |-  ( ( F e. B /\ c e. ( NN0 ^m 1o ) ) -> ( F ` c ) = ( ( coe1 ` F ) ` ( c ` (/) ) ) )
95 93 82 94 syl2anc 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( F ` c ) = ( ( coe1 ` F ) ` ( c ` (/) ) ) )
96 df1o2 
 |-  1o = { (/) }
97 0ex 
 |-  (/) e. _V
98 96 6 97 mapsnconst 
 |-  ( c e. ( NN0 ^m 1o ) -> c = ( 1o X. { ( c ` (/) ) } ) )
99 82 98 syl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> c = ( 1o X. { ( c ` (/) ) } ) )
100 99 oveq2d 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( ( 1o X. { k } ) oF - c ) = ( ( 1o X. { k } ) oF - ( 1o X. { ( c ` (/) ) } ) ) )
101 7 a1i 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> 1o e. On )
102 vex 
 |-  k e. _V
103 102 a1i 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> k e. _V )
104 fvexd 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( c ` (/) ) e. _V )
105 101 103 104 ofc12 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( ( 1o X. { k } ) oF - ( 1o X. { ( c ` (/) ) } ) ) = ( 1o X. { ( k - ( c ` (/) ) ) } ) )
106 100 105 eqtrd 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( ( 1o X. { k } ) oF - c ) = ( 1o X. { ( k - ( c ` (/) ) ) } ) )
107 106 fveq2d 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( G ` ( ( 1o X. { k } ) oF - c ) ) = ( G ` ( 1o X. { ( k - ( c ` (/) ) ) } ) ) )
108 simpll3 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> G e. B )
109 fznn0sub 
 |-  ( ( c ` (/) ) e. ( 0 ... k ) -> ( k - ( c ` (/) ) ) e. NN0 )
110 85 109 syl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( k - ( c ` (/) ) ) e. NN0 )
111 50 coe1fv 
 |-  ( ( G e. B /\ ( k - ( c ` (/) ) ) e. NN0 ) -> ( ( coe1 ` G ) ` ( k - ( c ` (/) ) ) ) = ( G ` ( 1o X. { ( k - ( c ` (/) ) ) } ) ) )
112 108 110 111 syl2anc 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( ( coe1 ` G ) ` ( k - ( c ` (/) ) ) ) = ( G ` ( 1o X. { ( k - ( c ` (/) ) ) } ) ) )
113 107 112 eqtr4d 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( G ` ( ( 1o X. { k } ) oF - c ) ) = ( ( coe1 ` G ) ` ( k - ( c ` (/) ) ) ) )
114 95 113 oveq12d 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) /\ c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } ) -> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) = ( ( ( coe1 ` F ) ` ( c ` (/) ) ) .x. ( ( coe1 ` G ) ` ( k - ( c ` (/) ) ) ) ) )
115 114 mpteq2dva 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) ) = ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( ( coe1 ` F ) ` ( c ` (/) ) ) .x. ( ( coe1 ` G ) ` ( k - ( c ` (/) ) ) ) ) ) )
116 92 115 eqtr4d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) o. ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( c ` (/) ) ) ) = ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) ) )
117 116 oveq2d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( R gsum ( ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) o. ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( c ` (/) ) ) ) ) = ( R gsum ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) ) ) )
118 75 117 eqtrd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ k e. NN0 ) -> ( R gsum ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) ) = ( R gsum ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) ) ) )
119 118 mpteq2dva 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( k e. NN0 |-> ( R gsum ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) ) ) = ( k e. NN0 |-> ( R gsum ( c e. { d e. ( NN0 ^m 1o ) | d oR <_ ( 1o X. { k } ) } |-> ( ( F ` c ) .x. ( G ` ( ( 1o X. { k } ) oF - c ) ) ) ) ) ) )
120 26 33 119 3eqtr4d 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .xb G ) ) = ( k e. NN0 |-> ( R gsum ( x e. ( 0 ... k ) |-> ( ( ( coe1 ` F ) ` x ) .x. ( ( coe1 ` G ) ` ( k - x ) ) ) ) ) ) )