Metamath Proof Explorer

Theorem m2cpmmhm

Description: The transformation of matrices into constant polynomial matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses m2cpm.s 
|- S = ( N ConstPolyMat R )
m2cpm.t 
|- T = ( N matToPolyMat R )
m2cpm.a 
|- A = ( N Mat R )
m2cpm.b 
|- B = ( Base ` A )
m2cpmghm.p 
|- P = ( Poly1 ` R )
m2cpmghm.c 
|- C = ( N Mat P )
m2cpmghm.u 
|- U = ( C |`s S )
Assertion m2cpmmhm 
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` U ) ) )

Proof

Step Hyp Ref Expression
1 m2cpm.s 
 |-  S = ( N ConstPolyMat R )
2 m2cpm.t 
 |-  T = ( N matToPolyMat R )
3 m2cpm.a 
 |-  A = ( N Mat R )
4 m2cpm.b 
 |-  B = ( Base ` A )
5 m2cpmghm.p 
 |-  P = ( Poly1 ` R )
6 m2cpmghm.c 
 |-  C = ( N Mat P )
7 m2cpmghm.u 
 |-  U = ( C |`s S )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 2 3 4 5 6 8 mat2pmatmhm 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) )
10 crngring 
 |-  ( R e. CRing -> R e. Ring )
11 10 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
12 1 5 6 cpmatsrgpmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubRing ` C ) )
13 eqid 
 |-  ( mulGrp ` C ) = ( mulGrp ` C )
14 13 subrgsubm 
 |-  ( S e. ( SubRing ` C ) -> S e. ( SubMnd ` ( mulGrp ` C ) ) )
15 11 12 14 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> S e. ( SubMnd ` ( mulGrp ` C ) ) )
16 1 2 3 4 m2cpmf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> S )
17 frn 
 |-  ( T : B --> S -> ran T C_ S )
18 11 16 17 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ran T C_ S )
19 6 ovexi 
 |-  C e. _V
20 1 ovexi 
 |-  S e. _V
21 7 13 mgpress 
 |-  ( ( C e. _V /\ S e. _V ) -> ( ( mulGrp ` C ) |`s S ) = ( mulGrp ` U ) )
22 19 20 21 mp2an 
 |-  ( ( mulGrp ` C ) |`s S ) = ( mulGrp ` U )
23 22 eqcomi 
 |-  ( mulGrp ` U ) = ( ( mulGrp ` C ) |`s S )
24 23 resmhm2b 
 |-  ( ( S e. ( SubMnd ` ( mulGrp ` C ) ) /\ ran T C_ S ) -> ( T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) <-> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` U ) ) ) )
25 15 18 24 syl2anc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) <-> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` U ) ) ) )
26 9 25 mpbid 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` U ) ) )