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 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
m2cpm.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
m2cpm.a 𝐴 = ( 𝑁 Mat 𝑅 )
m2cpm.b 𝐵 = ( Base ‘ 𝐴 )
m2cpmghm.p 𝑃 = ( Poly1𝑅 )
m2cpmghm.c 𝐶 = ( 𝑁 Mat 𝑃 )
m2cpmghm.u 𝑈 = ( 𝐶s 𝑆 )
Assertion m2cpmmhm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 m2cpm.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 m2cpm.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3 m2cpm.a 𝐴 = ( 𝑁 Mat 𝑅 )
4 m2cpm.b 𝐵 = ( Base ‘ 𝐴 )
5 m2cpmghm.p 𝑃 = ( Poly1𝑅 )
6 m2cpmghm.c 𝐶 = ( 𝑁 Mat 𝑃 )
7 m2cpmghm.u 𝑈 = ( 𝐶s 𝑆 )
8 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 2 3 4 5 6 8 mat2pmatmhm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) )
10 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
11 10 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
12 1 5 6 cpmatsrgpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubRing ‘ 𝐶 ) )
13 eqid ( mulGrp ‘ 𝐶 ) = ( mulGrp ‘ 𝐶 )
14 13 subrgsubm ( 𝑆 ∈ ( SubRing ‘ 𝐶 ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝐶 ) ) )
15 11 12 14 3syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝐶 ) ) )
16 1 2 3 4 m2cpmf ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵𝑆 )
17 frn ( 𝑇 : 𝐵𝑆 → ran 𝑇𝑆 )
18 11 16 17 3syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ran 𝑇𝑆 )
19 6 ovexi 𝐶 ∈ V
20 1 ovexi 𝑆 ∈ V
21 7 13 mgpress ( ( 𝐶 ∈ V ∧ 𝑆 ∈ V ) → ( ( mulGrp ‘ 𝐶 ) ↾s 𝑆 ) = ( mulGrp ‘ 𝑈 ) )
22 19 20 21 mp2an ( ( mulGrp ‘ 𝐶 ) ↾s 𝑆 ) = ( mulGrp ‘ 𝑈 )
23 22 eqcomi ( mulGrp ‘ 𝑈 ) = ( ( mulGrp ‘ 𝐶 ) ↾s 𝑆 )
24 23 resmhm2b ( ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝐶 ) ) ∧ ran 𝑇𝑆 ) → ( 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) ↔ 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) )
25 15 18 24 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) ↔ 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) )
26 9 25 mpbid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑈 ) ) )