Metamath Proof Explorer

Theorem mat2pmatmhm

Description: The transformation of matrices into polynomial matrices is a homomorphism of multiplicative monoids. (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 mat2pmatmhm 
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` 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 eqid 
 |-  ( mulGrp ` A ) = ( mulGrp ` A )
11 10 ringmgp 
 |-  ( A e. Ring -> ( mulGrp ` A ) e. Mnd )
12 9 11 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( mulGrp ` A ) e. Mnd )
13 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
14 7 13 syl 
 |-  ( R e. CRing -> P e. Ring )
15 5 matring 
 |-  ( ( N e. Fin /\ P e. Ring ) -> C e. Ring )
16 14 15 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> C e. Ring )
17 eqid 
 |-  ( mulGrp ` C ) = ( mulGrp ` C )
18 17 ringmgp 
 |-  ( C e. Ring -> ( mulGrp ` C ) e. Mnd )
19 16 18 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( mulGrp ` C ) e. Mnd )
20 1 2 3 4 5 6 mat2pmatf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> H )
21 7 20 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T : B --> H )
22 1 2 3 4 5 6 mat2pmatmul 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A. x e. B A. y e. B ( T ` ( x ( .r ` A ) y ) ) = ( ( T ` x ) ( .r ` C ) ( T ` y ) ) )
23 1 2 3 4 5 6 mat2pmat1 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` A ) ) = ( 1r ` C ) )
24 7 23 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( T ` ( 1r ` A ) ) = ( 1r ` C ) )
25 21 22 24 3jca 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( T : B --> H /\ A. x e. B A. y e. B ( T ` ( x ( .r ` A ) y ) ) = ( ( T ` x ) ( .r ` C ) ( T ` y ) ) /\ ( T ` ( 1r ` A ) ) = ( 1r ` C ) ) )
26 10 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` A ) )
27 17 6 mgpbas 
 |-  H = ( Base ` ( mulGrp ` C ) )
28 eqid 
 |-  ( .r ` A ) = ( .r ` A )
29 10 28 mgpplusg 
 |-  ( .r ` A ) = ( +g ` ( mulGrp ` A ) )
30 eqid 
 |-  ( .r ` C ) = ( .r ` C )
31 17 30 mgpplusg 
 |-  ( .r ` C ) = ( +g ` ( mulGrp ` C ) )
32 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
33 10 32 ringidval 
 |-  ( 1r ` A ) = ( 0g ` ( mulGrp ` A ) )
34 eqid 
 |-  ( 1r ` C ) = ( 1r ` C )
35 17 34 ringidval 
 |-  ( 1r ` C ) = ( 0g ` ( mulGrp ` C ) )
36 26 27 29 31 33 35 ismhm 
 |-  ( T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) <-> ( ( ( mulGrp ` A ) e. Mnd /\ ( mulGrp ` C ) e. Mnd ) /\ ( T : B --> H /\ A. x e. B A. y e. B ( T ` ( x ( .r ` A ) y ) ) = ( ( T ` x ) ( .r ` C ) ( T ` y ) ) /\ ( T ` ( 1r ` A ) ) = ( 1r ` C ) ) ) )
37 12 19 25 36 syl21anbrc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) )