Metamath Proof Explorer


Theorem mat2pmatrhm

Description: The transformation of matrices into polynomial matrices is a ring homomorphism. (Contributed by AV, 29-Oct-2019)

Ref Expression
Hypotheses mat2pmatbas.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
Assertion mat2pmatrhm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingHom 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2 mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
4 mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
5 mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
6 mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
7 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
8 2 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
9 7 8 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
10 4 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
11 7 10 syl ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
12 5 matring ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐶 ∈ Ring )
13 11 12 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ Ring )
14 1 2 3 4 5 6 mat2pmatghm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
15 7 14 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
16 1 2 3 4 5 6 mat2pmatmhm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) )
17 15 16 jca ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) ∧ 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) ) )
18 eqid ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
19 eqid ( mulGrp ‘ 𝐶 ) = ( mulGrp ‘ 𝐶 )
20 18 19 isrhm ( 𝑇 ∈ ( 𝐴 RingHom 𝐶 ) ↔ ( ( 𝐴 ∈ Ring ∧ 𝐶 ∈ Ring ) ∧ ( 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) ∧ 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) ) ) )
21 9 13 17 20 syl21anbrc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingHom 𝐶 ) )