# Metamath Proof Explorer

## Theorem pm2mpfo

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p
`|- P = ( Poly1 ` R )`
pm2mpfo.c
`|- C = ( N Mat P )`
pm2mpfo.b
`|- B = ( Base ` C )`
pm2mpfo.m
`|- .* = ( .s ` Q )`
pm2mpfo.e
`|- .^ = ( .g ` ( mulGrp ` Q ) )`
pm2mpfo.x
`|- X = ( var1 ` A )`
pm2mpfo.a
`|- A = ( N Mat R )`
pm2mpfo.q
`|- Q = ( Poly1 ` A )`
pm2mpfo.l
`|- L = ( Base ` Q )`
pm2mpfo.t
`|- T = ( N pMatToMatPoly R )`
Assertion pm2mpfo
`|- ( ( N e. Fin /\ R e. Ring ) -> T : B -onto-> L )`

### Proof

Step Hyp Ref Expression
1 pm2mpfo.p
` |-  P = ( Poly1 ` R )`
2 pm2mpfo.c
` |-  C = ( N Mat P )`
3 pm2mpfo.b
` |-  B = ( Base ` C )`
4 pm2mpfo.m
` |-  .* = ( .s ` Q )`
5 pm2mpfo.e
` |-  .^ = ( .g ` ( mulGrp ` Q ) )`
6 pm2mpfo.x
` |-  X = ( var1 ` A )`
7 pm2mpfo.a
` |-  A = ( N Mat R )`
8 pm2mpfo.q
` |-  Q = ( Poly1 ` A )`
9 pm2mpfo.l
` |-  L = ( Base ` Q )`
10 pm2mpfo.t
` |-  T = ( N pMatToMatPoly R )`
11 1 2 3 4 5 6 7 8 10 9 pm2mpf
` |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> L )`
12 eqid
` |-  ( .s ` P ) = ( .s ` P )`
13 eqid
` |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )`
14 eqid
` |-  ( var1 ` R ) = ( var1 ` R )`
15 eqid
` |-  ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) = ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) )`
16 7 8 9 12 13 14 15 1 10 mp2pm2mp
` |-  ( ( N e. Fin /\ R e. Ring /\ p e. L ) -> ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) = p )`
17 16 3expa
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) = p )`
18 7 8 9 1 12 13 14 15 2 3 mply1topmatcl
` |-  ( ( N e. Fin /\ R e. Ring /\ p e. L ) -> ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) e. B )`
19 18 3expa
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) e. B )`
20 simpr
` |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) /\ f = ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> f = ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) )`
21 20 fveq2d
` |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) /\ f = ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> ( T ` f ) = ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) )`
22 21 eqeq2d
` |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) /\ f = ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> ( p = ( T ` f ) <-> p = ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) ) )`
23 19 22 rspcedv
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> ( p = ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> E. f e. B p = ( T ` f ) ) )`
24 23 com12
` |-  ( p = ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> E. f e. B p = ( T ` f ) ) )`
25 24 eqcoms
` |-  ( ( T ` ( ( l e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` l ) ` k ) j ) ( .s ` P ) ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) ` p ) ) = p -> ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> E. f e. B p = ( T ` f ) ) )`
26 17 25 mpcom
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ p e. L ) -> E. f e. B p = ( T ` f ) )`
27 26 ralrimiva
` |-  ( ( N e. Fin /\ R e. Ring ) -> A. p e. L E. f e. B p = ( T ` f ) )`
28 dffo3
` |-  ( T : B -onto-> L <-> ( T : B --> L /\ A. p e. L E. f e. B p = ( T ` f ) ) )`
29 11 27 28 sylanbrc
` |-  ( ( N e. Fin /\ R e. Ring ) -> T : B -onto-> L )`