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

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 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
9 3 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
10 8 9 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
11 1 5 6 cpmatsrgpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubRing ‘ 𝐶 ) )
12 8 11 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ ( SubRing ‘ 𝐶 ) )
13 7 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐶 ) → 𝑈 ∈ Ring )
14 12 13 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ Ring )
15 1 2 3 4 5 6 7 m2cpmghm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) )
16 8 15 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) )
17 1 2 3 4 5 6 7 m2cpmmhm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑈 ) ) )
18 16 17 jca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) ∧ 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) )
19 eqid ⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
20 eqid ⊢ ( mulGrp ‘ 𝑈 ) = ( mulGrp ‘ 𝑈 )
21 19 20 isrhm ⊢ ( 𝑇 ∈ ( 𝐴 RingHom 𝑈 ) ↔ ( ( 𝐴 ∈ Ring ∧ 𝑈 ∈ Ring ) ∧ ( 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) ∧ 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) ) )
22 10 14 18 21 syl21anbrc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingHom 𝑈 ) )