Metamath Proof Explorer


Theorem pmatcollpw1lem2

Description: Lemma 2 for pmatcollpw1 : An entry of a polynomial matrix is the sum of the entries of the matrix consisting of the coefficients in the entries of the polynomial matrix multiplied with the corresponding power of the variable. (Contributed by AV, 25-Sep-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses pmatcollpw1.p
|- P = ( Poly1 ` R )
pmatcollpw1.c
|- C = ( N Mat P )
pmatcollpw1.b
|- B = ( Base ` C )
pmatcollpw1.m
|- .X. = ( .s ` P )
pmatcollpw1.e
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpw1.x
|- X = ( var1 ` R )
Assertion pmatcollpw1lem2
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a M b ) = ( P gsum ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw1.p
 |-  P = ( Poly1 ` R )
2 pmatcollpw1.c
 |-  C = ( N Mat P )
3 pmatcollpw1.b
 |-  B = ( Base ` C )
4 pmatcollpw1.m
 |-  .X. = ( .s ` P )
5 pmatcollpw1.e
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw1.x
 |-  X = ( var1 ` R )
7 simpl2
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> R e. Ring )
8 eqid
 |-  ( Base ` P ) = ( Base ` P )
9 simprl
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
10 simprr
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
11 simpl3
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> M e. B )
12 2 8 3 9 10 11 matecld
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a M b ) e. ( Base ` P ) )
13 eqid
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
14 eqid
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
15 eqid
 |-  ( coe1 ` ( a M b ) ) = ( coe1 ` ( a M b ) )
16 1 6 8 4 13 14 15 ply1coe
 |-  ( ( R e. Ring /\ ( a M b ) e. ( Base ` P ) ) -> ( a M b ) = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` ( a M b ) ) ` n ) .X. ( n ( .g ` ( mulGrp ` P ) ) X ) ) ) ) )
17 7 12 16 syl2anc
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a M b ) = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` ( a M b ) ) ` n ) .X. ( n ( .g ` ( mulGrp ` P ) ) X ) ) ) ) )
18 7 adantr
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> R e. Ring )
19 11 adantr
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> M e. B )
20 simpr
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> n e. NN0 )
21 simpr
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a e. N /\ b e. N ) )
22 21 adantr
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( a e. N /\ b e. N ) )
23 1 2 3 decpmate
 |-  ( ( ( R e. Ring /\ M e. B /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( a ( M decompPMat n ) b ) = ( ( coe1 ` ( a M b ) ) ` n ) )
24 18 19 20 22 23 syl31anc
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( a ( M decompPMat n ) b ) = ( ( coe1 ` ( a M b ) ) ` n ) )
25 24 eqcomd
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( a M b ) ) ` n ) = ( a ( M decompPMat n ) b ) )
26 5 eqcomi
 |-  ( .g ` ( mulGrp ` P ) ) = .^
27 26 oveqi
 |-  ( n ( .g ` ( mulGrp ` P ) ) X ) = ( n .^ X )
28 27 a1i
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( n ( .g ` ( mulGrp ` P ) ) X ) = ( n .^ X ) )
29 25 28 oveq12d
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( ( coe1 ` ( a M b ) ) ` n ) .X. ( n ( .g ` ( mulGrp ` P ) ) X ) ) = ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) )
30 29 mpteq2dva
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( n e. NN0 |-> ( ( ( coe1 ` ( a M b ) ) ` n ) .X. ( n ( .g ` ( mulGrp ` P ) ) X ) ) ) = ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) )
31 30 oveq2d
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` ( a M b ) ) ` n ) .X. ( n ( .g ` ( mulGrp ` P ) ) X ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) ) )
32 17 31 eqtrd
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a M b ) = ( P gsum ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) ) )