Metamath Proof Explorer

Theorem pmatcollpw

Description: Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 26-Oct-2019) (Revised by AV, 4-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 pmatcollpw.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpw.c 
 |-  C = ( N Mat P )
3 pmatcollpw.b 
 |-  B = ( Base ` C )
4 pmatcollpw.m 
 |-  .* = ( .s ` C )
5 pmatcollpw.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw.x 
 |-  X = ( var1 ` R )
7 pmatcollpw.t 
 |-  T = ( N matToPolyMat R )
8 crngring 
 |-  ( R e. CRing -> R e. Ring )
9 eqid 
 |-  ( .s ` P ) = ( .s ` P )
10 1 2 3 9 5 6 pmatcollpw2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M = ( C gsum ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) ) ) )
11 8 10 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M = ( C gsum ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) ) ) )
12 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) = ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) )
13 oveq12 
 |-  ( ( i = a /\ j = b ) -> ( i ( M decompPMat n ) j ) = ( a ( M decompPMat n ) b ) )
14 13 oveq1d 
 |-  ( ( i = a /\ j = b ) -> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) = ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) )
15 14 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) /\ ( i = a /\ j = b ) ) -> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) = ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) )
16 simprl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
17 simpr 
 |-  ( ( a e. N /\ b e. N ) -> b e. N )
18 17 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
19 simp2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. CRing )
20 19 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> R e. CRing )
21 20 8 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> R e. Ring )
22 21 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> R e. Ring )
23 eqid 
 |-  ( N Mat R ) = ( N Mat R )
24 eqid 
 |-  ( Base ` R ) = ( Base ` R )
25 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
26 simp3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M e. B )
27 26 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> M e. B )
28 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> n e. NN0 )
29 1 2 3 23 25 decpmatcl 
 |-  ( ( R e. CRing /\ M e. B /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
30 20 27 28 29 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
31 30 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
32 23 24 25 16 18 31 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( a ( M decompPMat n ) b ) e. ( Base ` R ) )
33 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> n e. NN0 )
34 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
35 eqid 
 |-  ( Base ` P ) = ( Base ` P )
36 24 1 6 9 34 5 35 ply1tmcl 
 |-  ( ( R e. Ring /\ ( a ( M decompPMat n ) b ) e. ( Base ` R ) /\ n e. NN0 ) -> ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) e. ( Base ` P ) )
37 22 32 33 36 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) e. ( Base ` P ) )
38 12 15 16 18 37 ovmpod 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( a ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) b ) = ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) )
39 1 2 3 4 5 6 7 pmatcollpwlem 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )
40 39 3expb 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )
41 38 40 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ ( a e. N /\ b e. N ) ) -> ( a ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) b ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )
42 41 ralrimivva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> A. a e. N A. b e. N ( a ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) b ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )
43 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> N e. Fin )
44 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
45 8 44 syl 
 |-  ( R e. CRing -> P e. Ring )
46 45 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
47 46 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> P e. Ring )
48 21 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
49 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
50 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> j e. N )
51 30 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
52 23 24 25 49 50 51 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( i ( M decompPMat n ) j ) e. ( Base ` R ) )
53 28 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> n e. NN0 )
54 24 1 6 9 34 5 35 ply1tmcl 
 |-  ( ( R e. Ring /\ ( i ( M decompPMat n ) j ) e. ( Base ` R ) /\ n e. NN0 ) -> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) e. ( Base ` P ) )
55 48 52 53 54 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) e. ( Base ` P ) )
56 2 35 3 43 47 55 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) e. B )
57 8 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
58 1 6 34 5 35 ply1moncl 
 |-  ( ( R e. Ring /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` P ) )
59 57 58 sylan 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` P ) )
60 57 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> R e. Ring )
61 7 23 25 1 2 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) ) -> ( T ` ( M decompPMat n ) ) e. ( Base ` C ) )
62 43 60 30 61 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( T ` ( M decompPMat n ) ) e. ( Base ` C ) )
63 62 3 eleqtrrdi 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( T ` ( M decompPMat n ) ) e. B )
64 35 2 3 4 matvscl 
 |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( ( n .^ X ) e. ( Base ` P ) /\ ( T ` ( M decompPMat n ) ) e. B ) ) -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) e. B )
65 43 47 59 63 64 syl22anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) e. B )
66 2 3 eqmat 
 |-  ( ( ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) e. B /\ ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) e. B ) -> ( ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) = ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) <-> A. a e. N A. b e. N ( a ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) b ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) ) )
67 56 65 66 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) = ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) <-> A. a e. N A. b e. N ( a ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) b ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) ) )
68 42 67 mpbird 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) = ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) )
69 68 mpteq2dva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) ) = ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) )
70 69 oveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C gsum ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) ( .s ` P ) ( n .^ X ) ) ) ) ) = ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
71 11 70 eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M = ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )