Metamath Proof Explorer

Theorem pm2mprhm

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

Ref Expression
Hypotheses pm2mpmhm.p ⊢ P = Poly 1 ⁡ R
pm2mpmhm.c ⊢ C = N Mat P
pm2mpmhm.a ⊢ A = N Mat R
pm2mpmhm.q ⊢ Q = Poly 1 ⁡ A
pm2mpmhm.t ⊢ T = N pMatToMatPoly R
Assertion pm2mprhm ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ C RingHom Q

Proof

Step Hyp Ref Expression
1 pm2mpmhm.p ⊢ P = Poly 1 ⁡ R
2 pm2mpmhm.c ⊢ C = N Mat P
3 pm2mpmhm.a ⊢ A = N Mat R
4 pm2mpmhm.q ⊢ Q = Poly 1 ⁡ A
5 pm2mpmhm.t ⊢ T = N pMatToMatPoly R
6 1 2 pmatring ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ Ring
7 3 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
8 4 ply1ring ⊢ A ∈ Ring → Q ∈ Ring
9 7 8 syl ⊢ N ∈ Fin ∧ R ∈ Ring → Q ∈ Ring
10 eqid ⊢ Base C = Base C
11 eqid ⊢ ⋅ Q = ⋅ Q
12 eqid ⊢ ⋅ mulGrp Q = ⋅ mulGrp Q
13 eqid ⊢ var 1 ⁡ A = var 1 ⁡ A
14 eqid ⊢ Base Q = Base Q
15 1 2 10 11 12 13 3 4 14 5 pm2mpghm ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ C GrpHom Q
16 1 2 3 4 5 pm2mpmhm ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ mulGrp C MndHom mulGrp Q
17 15 16 jca ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ C GrpHom Q ∧ T ∈ mulGrp C MndHom mulGrp Q
18 eqid ⊢ mulGrp C = mulGrp C
19 eqid ⊢ mulGrp Q = mulGrp Q
20 18 19 isrhm ⊢ T ∈ C RingHom Q ↔ C ∈ Ring ∧ Q ∈ Ring ∧ T ∈ C GrpHom Q ∧ T ∈ mulGrp C MndHom mulGrp Q
21 6 9 17 20 syl21anbrc ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ C RingHom Q