Metamath Proof Explorer

Theorem pmatcollpw1

Description: Write a polynomial matrix as a matrix of sums of scaled monomials. (Contributed by AV, 29-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 pmatcollpw1 
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M = ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .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 1 2 3 4 5 6 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 ) ) ) ) )
8 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) = ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) )
9 oveq12 
 |-  ( ( i = a /\ j = b ) -> ( i ( M decompPMat n ) j ) = ( a ( M decompPMat n ) b ) )
10 9 oveq1d 
 |-  ( ( i = a /\ j = b ) -> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) = ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) )
11 10 mpteq2dv 
 |-  ( ( i = a /\ j = b ) -> ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) = ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) )
12 11 oveq2d 
 |-  ( ( i = a /\ j = b ) -> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) ) )
13 12 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ ( i = a /\ j = b ) ) -> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) ) )
14 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
15 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
16 eqid 
 |-  ( Base ` P ) = ( Base ` P )
17 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
18 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
19 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
20 18 19 syl 
 |-  ( R e. Ring -> P e. CMnd )
21 20 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. CMnd )
22 21 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> P e. CMnd )
23 nn0ex 
 |-  NN0 e. _V
24 23 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> NN0 e. _V )
25 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> R e. Ring )
26 25 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> R e. Ring )
27 eqid 
 |-  ( N Mat R ) = ( N Mat R )
28 eqid 
 |-  ( Base ` R ) = ( Base ` R )
29 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
30 simplrl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> a e. N )
31 15 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> b e. N )
32 simpl3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> M e. B )
33 32 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> M e. B )
34 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> n e. NN0 )
35 1 2 3 27 29 decpmatcl 
 |-  ( ( R e. Ring /\ M e. B /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
36 26 33 34 35 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
37 27 28 29 30 31 36 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( a ( M decompPMat n ) b ) e. ( Base ` R ) )
38 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
39 28 1 6 4 38 5 16 ply1tmcl 
 |-  ( ( R e. Ring /\ ( a ( M decompPMat n ) b ) e. ( Base ` R ) /\ n e. NN0 ) -> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) e. ( Base ` P ) )
40 26 37 34 39 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) e. ( Base ` P ) )
41 40 fmpttd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) : NN0 --> ( Base ` P ) )
42 1 2 3 4 5 6 pmatcollpw1lem1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ a e. N /\ b e. N ) -> ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) finSupp ( 0g ` P ) )
43 42 3expb 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) finSupp ( 0g ` P ) )
44 16 17 22 24 41 43 gsumcl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( P gsum ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) ) e. ( Base ` P ) )
45 8 13 14 15 44 ovmpod 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) b ) = ( P gsum ( n e. NN0 |-> ( ( a ( M decompPMat n ) b ) .X. ( n .^ X ) ) ) ) )
46 7 45 eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a M b ) = ( a ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) b ) )
47 46 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> A. a e. N A. b e. N ( a M b ) = ( a ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) b ) )
48 simp3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M e. B )
49 simp1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> N e. Fin )
50 18 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. Ring )
51 21 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) -> P e. CMnd )
52 23 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) -> NN0 e. _V )
53 simpl12 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) /\ n e. NN0 ) -> R e. Ring )
54 simpl2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) /\ n e. NN0 ) -> i e. N )
55 simpl3 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) /\ n e. NN0 ) -> j e. N )
56 48 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) -> M e. B )
57 56 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) /\ n e. NN0 ) -> M e. B )
58 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) /\ n e. NN0 ) -> n e. NN0 )
59 53 57 58 35 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
60 27 28 29 54 55 59 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) /\ n e. NN0 ) -> ( i ( M decompPMat n ) j ) e. ( Base ` R ) )
61 28 1 6 4 38 5 16 ply1tmcl 
 |-  ( ( R e. Ring /\ ( i ( M decompPMat n ) j ) e. ( Base ` R ) /\ n e. NN0 ) -> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) e. ( Base ` P ) )
62 53 60 58 61 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) /\ n e. NN0 ) -> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) e. ( Base ` P ) )
63 62 fmpttd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) -> ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) : NN0 --> ( Base ` P ) )
64 1 2 3 4 5 6 pmatcollpw1lem1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) -> ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) finSupp ( 0g ` P ) )
65 16 17 51 52 63 64 gsumcl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ i e. N /\ j e. N ) -> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) e. ( Base ` P ) )
66 2 16 3 49 50 65 matbas2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) e. B )
67 2 3 eqmat 
 |-  ( ( M e. B /\ ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) e. B ) -> ( M = ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) <-> A. a e. N A. b e. N ( a M b ) = ( a ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) b ) ) )
68 48 66 67 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( M = ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) <-> A. a e. N A. b e. N ( a M b ) = ( a ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) b ) ) )
69 47 68 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M = ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) )