Metamath Proof Explorer

Theorem m2cpmrhm

Description: The transformation of matrices into constant polynomial matrices is a ring homomorphism. (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 m2cpmrhm 
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom 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 crngring 
 |-  ( R e. CRing -> R e. Ring )
9 3 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
10 8 9 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
11 1 5 6 cpmatsrgpmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubRing ` C ) )
12 8 11 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> S e. ( SubRing ` C ) )
13 7 subrgring 
 |-  ( S e. ( SubRing ` C ) -> U e. Ring )
14 12 13 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> U e. Ring )
15 1 2 3 4 5 6 7 m2cpmghm 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom U ) )
16 8 15 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A GrpHom U ) )
17 1 2 3 4 5 6 7 m2cpmmhm 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` U ) ) )
18 16 17 jca 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( T e. ( A GrpHom U ) /\ T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` U ) ) ) )
19 eqid 
 |-  ( mulGrp ` A ) = ( mulGrp ` A )
20 eqid 
 |-  ( mulGrp ` U ) = ( mulGrp ` U )
21 19 20 isrhm 
 |-  ( T e. ( A RingHom U ) <-> ( ( A e. Ring /\ U e. Ring ) /\ ( T e. ( A GrpHom U ) /\ T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` U ) ) ) ) )
22 10 14 18 21 syl21anbrc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom U ) )