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 ) ) ) ) )