Metamath Proof Explorer

Theorem pm2mpmhm

Description: The transformation of polynomial matrices into polynomials over matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 22-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpmhm.p 
|- P = ( Poly1 ` R )
pm2mpmhm.c 
|- C = ( N Mat P )
pm2mpmhm.a 
|- A = ( N Mat R )
pm2mpmhm.q 
|- Q = ( Poly1 ` A )
pm2mpmhm.t 
|- T = ( N pMatToMatPoly R )
Assertion pm2mpmhm 
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( ( mulGrp ` C ) MndHom ( mulGrp ` Q ) ) )

Proof

Step Hyp Ref Expression
1 pm2mpmhm.p 
 |-  P = ( Poly1 ` R )
2 pm2mpmhm.c 
 |-  C = ( N Mat P )
3 pm2mpmhm.a 
 |-  A = ( N Mat R )
4 pm2mpmhm.q 
 |-  Q = ( Poly1 ` A )
5 pm2mpmhm.t 
 |-  T = ( N pMatToMatPoly R )
6 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
7 eqid 
 |-  ( mulGrp ` C ) = ( mulGrp ` C )
8 7 ringmgp 
 |-  ( C e. Ring -> ( mulGrp ` C ) e. Mnd )
9 6 8 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( mulGrp ` C ) e. Mnd )
10 3 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
11 4 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
12 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
13 12 ringmgp 
 |-  ( Q e. Ring -> ( mulGrp ` Q ) e. Mnd )
14 10 11 13 3syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( mulGrp ` Q ) e. Mnd )
15 eqid 
 |-  ( Base ` C ) = ( Base ` C )
16 7 15 mgpbas 
 |-  ( Base ` C ) = ( Base ` ( mulGrp ` C ) )
17 16 eqcomi 
 |-  ( Base ` ( mulGrp ` C ) ) = ( Base ` C )
18 eqid 
 |-  ( .s ` Q ) = ( .s ` Q )
19 eqid 
 |-  ( .g ` ( mulGrp ` Q ) ) = ( .g ` ( mulGrp ` Q ) )
20 eqid 
 |-  ( var1 ` A ) = ( var1 ` A )
21 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
22 12 21 mgpbas 
 |-  ( Base ` Q ) = ( Base ` ( mulGrp ` Q ) )
23 22 eqcomi 
 |-  ( Base ` ( mulGrp ` Q ) ) = ( Base ` Q )
24 1 2 17 18 19 20 3 4 5 23 pm2mpf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : ( Base ` ( mulGrp ` C ) ) --> ( Base ` ( mulGrp ` Q ) ) )
25 1 2 3 4 5 17 pm2mpmhmlem2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. ( Base ` ( mulGrp ` C ) ) A. y e. ( Base ` ( mulGrp ` C ) ) ( T ` ( x ( .r ` C ) y ) ) = ( ( T ` x ) ( .r ` Q ) ( T ` y ) ) )
26 1 2 15 18 19 20 3 4 5 idpm2idmp 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` C ) ) = ( 1r ` Q ) )
27 24 25 26 3jca 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T : ( Base ` ( mulGrp ` C ) ) --> ( Base ` ( mulGrp ` Q ) ) /\ A. x e. ( Base ` ( mulGrp ` C ) ) A. y e. ( Base ` ( mulGrp ` C ) ) ( T ` ( x ( .r ` C ) y ) ) = ( ( T ` x ) ( .r ` Q ) ( T ` y ) ) /\ ( T ` ( 1r ` C ) ) = ( 1r ` Q ) ) )
28 eqid 
 |-  ( Base ` ( mulGrp ` C ) ) = ( Base ` ( mulGrp ` C ) )
29 eqid 
 |-  ( Base ` ( mulGrp ` Q ) ) = ( Base ` ( mulGrp ` Q ) )
30 eqid 
 |-  ( .r ` C ) = ( .r ` C )
31 7 30 mgpplusg 
 |-  ( .r ` C ) = ( +g ` ( mulGrp ` C ) )
32 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
33 12 32 mgpplusg 
 |-  ( .r ` Q ) = ( +g ` ( mulGrp ` Q ) )
34 eqid 
 |-  ( 1r ` C ) = ( 1r ` C )
35 7 34 ringidval 
 |-  ( 1r ` C ) = ( 0g ` ( mulGrp ` C ) )
36 eqid 
 |-  ( 1r ` Q ) = ( 1r ` Q )
37 12 36 ringidval 
 |-  ( 1r ` Q ) = ( 0g ` ( mulGrp ` Q ) )
38 28 29 31 33 35 37 ismhm 
 |-  ( T e. ( ( mulGrp ` C ) MndHom ( mulGrp ` Q ) ) <-> ( ( ( mulGrp ` C ) e. Mnd /\ ( mulGrp ` Q ) e. Mnd ) /\ ( T : ( Base ` ( mulGrp ` C ) ) --> ( Base ` ( mulGrp ` Q ) ) /\ A. x e. ( Base ` ( mulGrp ` C ) ) A. y e. ( Base ` ( mulGrp ` C ) ) ( T ` ( x ( .r ` C ) y ) ) = ( ( T ` x ) ( .r ` Q ) ( T ` y ) ) /\ ( T ` ( 1r ` C ) ) = ( 1r ` Q ) ) ) )
39 9 14 27 38 syl21anbrc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( ( mulGrp ` C ) MndHom ( mulGrp ` Q ) ) )