Metamath Proof Explorer

Theorem pm2mprhm

Description: The transformation of polynomial matrices into polynomials over matrices is a ring homomorphism. (Contributed by AV, 22-Oct-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 pm2mprhm 
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingHom 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 3 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
8 4 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
9 7 8 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
10 eqid 
 |-  ( Base ` C ) = ( Base ` C )
11 eqid 
 |-  ( .s ` Q ) = ( .s ` Q )
12 eqid 
 |-  ( .g ` ( mulGrp ` Q ) ) = ( .g ` ( mulGrp ` Q ) )
13 eqid 
 |-  ( var1 ` A ) = ( var1 ` A )
14 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
15 1 2 10 11 12 13 3 4 14 5 pm2mpghm 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( C GrpHom Q ) )
16 1 2 3 4 5 pm2mpmhm 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( ( mulGrp ` C ) MndHom ( mulGrp ` Q ) ) )
17 15 16 jca 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T e. ( C GrpHom Q ) /\ T e. ( ( mulGrp ` C ) MndHom ( mulGrp ` Q ) ) ) )
18 eqid 
 |-  ( mulGrp ` C ) = ( mulGrp ` C )
19 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
20 18 19 isrhm 
 |-  ( T e. ( C RingHom Q ) <-> ( ( C e. Ring /\ Q e. Ring ) /\ ( T e. ( C GrpHom Q ) /\ T e. ( ( mulGrp ` C ) MndHom ( mulGrp ` Q ) ) ) ) )
21 6 9 17 20 syl21anbrc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingHom Q ) )