Metamath Proof Explorer

Theorem mp2pm2mp

Description: A polynomial over matrices transformed into a polynomial matrix transformed back into the polynomial over matrices. (Contributed by AV, 12-Oct-2019)

Ref Expression
Hypotheses mp2pm2mp.a 
|- A = ( N Mat R )
mp2pm2mp.q 
|- Q = ( Poly1 ` A )
mp2pm2mp.l 
|- L = ( Base ` Q )
mp2pm2mp.m 
|- .x. = ( .s ` P )
mp2pm2mp.e 
|- E = ( .g ` ( mulGrp ` P ) )
mp2pm2mp.y 
|- Y = ( var1 ` R )
mp2pm2mp.i 
|- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
mp2pm2mplem2.p 
|- P = ( Poly1 ` R )
mp2pm2mp.t 
|- T = ( N pMatToMatPoly R )
Assertion mp2pm2mp 
|- ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( T ` ( I ` O ) ) = O )

Proof

Step Hyp Ref Expression
1 mp2pm2mp.a 
 |-  A = ( N Mat R )
2 mp2pm2mp.q 
 |-  Q = ( Poly1 ` A )
3 mp2pm2mp.l 
 |-  L = ( Base ` Q )
4 mp2pm2mp.m 
 |-  .x. = ( .s ` P )
5 mp2pm2mp.e 
 |-  E = ( .g ` ( mulGrp ` P ) )
6 mp2pm2mp.y 
 |-  Y = ( var1 ` R )
7 mp2pm2mp.i 
 |-  I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
8 mp2pm2mplem2.p 
 |-  P = ( Poly1 ` R )
9 mp2pm2mp.t 
 |-  T = ( N pMatToMatPoly R )
10 eqid 
 |-  ( N Mat P ) = ( N Mat P )
11 eqid 
 |-  ( Base ` ( N Mat P ) ) = ( Base ` ( N Mat P ) )
12 1 2 3 8 4 5 6 7 10 11 mply1topmatcl 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( I ` O ) e. ( Base ` ( N Mat P ) ) )
13 eqid 
 |-  ( .s ` Q ) = ( .s ` Q )
14 eqid 
 |-  ( .g ` ( mulGrp ` Q ) ) = ( .g ` ( mulGrp ` Q ) )
15 eqid 
 |-  ( var1 ` A ) = ( var1 ` A )
16 8 10 11 13 14 15 1 2 9 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( I ` O ) e. ( Base ` ( N Mat P ) ) ) -> ( T ` ( I ` O ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
17 12 16 syld3an3 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( T ` ( I ` O ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
18 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
19 18 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> A e. Ring )
20 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
21 2 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
22 ringcmn 
 |-  ( Q e. Ring -> Q e. CMnd )
23 18 21 22 3syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. CMnd )
24 23 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> Q e. CMnd )
25 nn0ex 
 |-  NN0 e. _V
26 25 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> NN0 e. _V )
27 19 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ n e. NN0 ) -> A e. Ring )
28 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ n e. NN0 ) -> R e. Ring )
29 12 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ n e. NN0 ) -> ( I ` O ) e. ( Base ` ( N Mat P ) ) )
30 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ n e. NN0 ) -> n e. NN0 )
31 eqid 
 |-  ( Base ` A ) = ( Base ` A )
32 8 10 11 1 31 decpmatcl 
 |-  ( ( R e. Ring /\ ( I ` O ) e. ( Base ` ( N Mat P ) ) /\ n e. NN0 ) -> ( ( I ` O ) decompPMat n ) e. ( Base ` A ) )
33 28 29 30 32 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ n e. NN0 ) -> ( ( I ` O ) decompPMat n ) e. ( Base ` A ) )
34 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
35 31 2 15 13 34 14 3 ply1tmcl 
 |-  ( ( A e. Ring /\ ( ( I ` O ) decompPMat n ) e. ( Base ` A ) /\ n e. NN0 ) -> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. L )
36 27 33 30 35 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ n e. NN0 ) -> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) e. L )
37 36 fmpttd 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) : NN0 --> L )
38 fveq2 
 |-  ( k = n -> ( ( coe1 ` p ) ` k ) = ( ( coe1 ` p ) ` n ) )
39 38 oveqd 
 |-  ( k = n -> ( i ( ( coe1 ` p ) ` k ) j ) = ( i ( ( coe1 ` p ) ` n ) j ) )
40 oveq1 
 |-  ( k = n -> ( k E Y ) = ( n E Y ) )
41 39 40 oveq12d 
 |-  ( k = n -> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) = ( ( i ( ( coe1 ` p ) ` n ) j ) .x. ( n E Y ) ) )
42 41 cbvmptv 
 |-  ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) = ( n e. NN0 |-> ( ( i ( ( coe1 ` p ) ` n ) j ) .x. ( n E Y ) ) )
43 42 a1i 
 |-  ( ( i e. N /\ j e. N ) -> ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) = ( n e. NN0 |-> ( ( i ( ( coe1 ` p ) ` n ) j ) .x. ( n E Y ) ) ) )
44 43 oveq2d 
 |-  ( ( i e. N /\ j e. N ) -> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( i ( ( coe1 ` p ) ` n ) j ) .x. ( n E Y ) ) ) ) )
45 44 mpoeq3ia 
 |-  ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) = ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( ( coe1 ` p ) ` n ) j ) .x. ( n E Y ) ) ) ) )
46 45 mpteq2i 
 |-  ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) ) = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( ( coe1 ` p ) ` n ) j ) .x. ( n E Y ) ) ) ) ) )
47 7 46 eqtri 
 |-  I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( ( coe1 ` p ) ` n ) j ) .x. ( n E Y ) ) ) ) ) )
48 1 2 3 4 5 6 47 8 13 14 15 mp2pm2mplem5 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) finSupp ( 0g ` Q ) )
49 3 20 24 26 37 48 gsumcl 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. L )
50 simp3 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> O e. L )
51 19 49 50 3jca 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( A e. Ring /\ ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. L /\ O e. L ) )
52 1 2 3 4 5 6 7 8 mp2pm2mplem4 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ n e. NN0 ) -> ( ( I ` O ) decompPMat n ) = ( ( coe1 ` O ) ` n ) )
53 52 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ n e. NN0 ) -> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) = ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) )
54 53 adantlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) /\ n e. NN0 ) -> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) = ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) )
55 54 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) = ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) )
56 55 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
57 56 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) = ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) )
58 57 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) = ( ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) )
59 19 50 jca 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( A e. Ring /\ O e. L ) )
60 59 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( A e. Ring /\ O e. L ) )
61 eqid 
 |-  ( coe1 ` O ) = ( coe1 ` O )
62 2 15 3 13 34 14 61 ply1coe 
 |-  ( ( A e. Ring /\ O e. L ) -> O = ( Q gsum ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
63 60 62 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> O = ( Q gsum ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
64 63 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( Q gsum ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) = O )
65 64 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) = ( coe1 ` O ) )
66 65 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( coe1 ` O ) ` n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) = ( ( coe1 ` O ) ` l ) )
67 58 66 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ l e. NN0 ) -> ( ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) = ( ( coe1 ` O ) ` l ) )
68 67 ralrimiva 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> A. l e. NN0 ( ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) = ( ( coe1 ` O ) ` l ) )
69 eqid 
 |-  ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) = ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) )
70 2 3 69 61 eqcoe1ply1eq 
 |-  ( ( A e. Ring /\ ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) e. L /\ O e. L ) -> ( A. l e. NN0 ( ( coe1 ` ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) ) ` l ) = ( ( coe1 ` O ) ` l ) -> ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) = O ) )
71 51 68 70 sylc 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( Q gsum ( n e. NN0 |-> ( ( ( I ` O ) decompPMat n ) ( .s ` Q ) ( n ( .g ` ( mulGrp ` Q ) ) ( var1 ` A ) ) ) ) ) = O )
72 17 71 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( T ` ( I ` O ) ) = O )