Metamath Proof Explorer


Theorem mat2pmatrhm

Description: The transformation of matrices into polynomial matrices is a ring homomorphism. (Contributed by AV, 29-Oct-2019)

Ref Expression
Hypotheses mat2pmatbas.t
|- T = ( N matToPolyMat R )
mat2pmatbas.a
|- A = ( N Mat R )
mat2pmatbas.b
|- B = ( Base ` A )
mat2pmatbas.p
|- P = ( Poly1 ` R )
mat2pmatbas.c
|- C = ( N Mat P )
mat2pmatbas0.h
|- H = ( Base ` C )
Assertion mat2pmatrhm
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom C ) )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t
 |-  T = ( N matToPolyMat R )
2 mat2pmatbas.a
 |-  A = ( N Mat R )
3 mat2pmatbas.b
 |-  B = ( Base ` A )
4 mat2pmatbas.p
 |-  P = ( Poly1 ` R )
5 mat2pmatbas.c
 |-  C = ( N Mat P )
6 mat2pmatbas0.h
 |-  H = ( Base ` C )
7 crngring
 |-  ( R e. CRing -> R e. Ring )
8 2 matring
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
9 7 8 sylan2
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
10 4 ply1ring
 |-  ( R e. Ring -> P e. Ring )
11 7 10 syl
 |-  ( R e. CRing -> P e. Ring )
12 5 matring
 |-  ( ( N e. Fin /\ P e. Ring ) -> C e. Ring )
13 11 12 sylan2
 |-  ( ( N e. Fin /\ R e. CRing ) -> C e. Ring )
14 1 2 3 4 5 6 mat2pmatghm
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) )
15 7 14 sylan2
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A GrpHom C ) )
16 1 2 3 4 5 6 mat2pmatmhm
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) )
17 15 16 jca
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( T e. ( A GrpHom C ) /\ T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) ) )
18 eqid
 |-  ( mulGrp ` A ) = ( mulGrp ` A )
19 eqid
 |-  ( mulGrp ` C ) = ( mulGrp ` C )
20 18 19 isrhm
 |-  ( T e. ( A RingHom C ) <-> ( ( A e. Ring /\ C e. Ring ) /\ ( T e. ( A GrpHom C ) /\ T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) ) ) )
21 9 13 17 20 syl21anbrc
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom C ) )