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 ‘ 𝑈 ) ) )