Metamath Proof Explorer

Theorem pm2mprngiso

Description: The transformation of polynomial matrices into polynomials over matrices is a ring isomorphism. (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 pm2mprngiso ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ C RingIso 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 3 4 5 pm2mprhm ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ C RingHom Q
7 eqid ⊢ Base C = Base C
8 eqid ⊢ ⋅ Q = ⋅ Q
9 eqid ⊢ ⋅ mulGrp Q = ⋅ mulGrp Q
10 eqid ⊢ var 1 ⁡ A = var 1 ⁡ A
11 eqid ⊢ Base Q = Base Q
12 1 2 7 8 9 10 3 4 11 5 pm2mpf1o ⊢ N ∈ Fin ∧ R ∈ Ring → T : Base C ⟶ 1-1 onto Base Q
13 1 2 pmatring ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ Ring
14 3 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
15 4 ply1ring ⊢ A ∈ Ring → Q ∈ Ring
16 14 15 syl ⊢ N ∈ Fin ∧ R ∈ Ring → Q ∈ Ring
17 7 11 isrim ⊢ C ∈ Ring ∧ Q ∈ Ring → T ∈ C RingIso Q ↔ T ∈ C RingHom Q ∧ T : Base C ⟶ 1-1 onto Base Q
18 13 16 17 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ C RingIso Q ↔ T ∈ C RingHom Q ∧ T : Base C ⟶ 1-1 onto Base Q
19 6 12 18 mpbir2and ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ C RingIso Q