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 ⊢ T = N matToPolyMat R
mat2pmatbas.a ⊢ A = N Mat R
mat2pmatbas.b ⊢ B = Base A
mat2pmatbas.p ⊢ P = Poly 1 ⁡ R
mat2pmatbas.c ⊢ C = N Mat P
mat2pmatbas0.h ⊢ H = Base C
Assertion mat2pmatrhm ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A RingHom C

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t ⊢ T = N matToPolyMat R
2 mat2pmatbas.a ⊢ A = N Mat R
3 mat2pmatbas.b ⊢ B = Base A
4 mat2pmatbas.p ⊢ P = Poly 1 ⁡ R
5 mat2pmatbas.c ⊢ C = N Mat P
6 mat2pmatbas0.h ⊢ H = Base C
7 crngring ⊢ R ∈ CRing → R ∈ Ring
8 2 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
9 7 8 sylan2 ⊢ N ∈ Fin ∧ R ∈ CRing → A ∈ Ring
10 4 ply1ring ⊢ R ∈ Ring → P ∈ Ring
11 7 10 syl ⊢ R ∈ CRing → P ∈ Ring
12 5 matring ⊢ N ∈ Fin ∧ P ∈ Ring → C ∈ Ring
13 11 12 sylan2 ⊢ N ∈ Fin ∧ R ∈ CRing → C ∈ Ring
14 1 2 3 4 5 6 mat2pmatghm ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ A GrpHom C
15 7 14 sylan2 ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A GrpHom C
16 1 2 3 4 5 6 mat2pmatmhm ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ mulGrp A MndHom mulGrp C
17 15 16 jca ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A GrpHom C ∧ T ∈ mulGrp A MndHom mulGrp C
18 eqid ⊢ mulGrp A = mulGrp A
19 eqid ⊢ mulGrp C = mulGrp C
20 18 19 isrhm ⊢ T ∈ A RingHom C ↔ A ∈ Ring ∧ C ∈ Ring ∧ T ∈ A GrpHom C ∧ T ∈ mulGrp A MndHom mulGrp C
21 9 13 17 20 syl21anbrc ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A RingHom C