Metamath Proof Explorer

Theorem m2cpmrngiso

Description: The transformation of matrices into constant polynomial matrices is a ring isomorphism. (Contributed by AV, 19-Nov-2019)

Ref Expression
Hypotheses m2cpmfo.s ⊢ S = N ConstPolyMat R
m2cpmfo.t ⊢ T = N matToPolyMat R
m2cpmfo.a ⊢ A = N Mat R
m2cpmfo.k ⊢ K = Base A
m2cpmrngiso.p ⊢ P = Poly 1 ⁡ R
m2cpmrngiso.c ⊢ C = N Mat P
m2cpmrngiso.u ⊢ U = C ↾ 𝑠 S
Assertion m2cpmrngiso ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A RingIso U

Proof

Step Hyp Ref Expression
1 m2cpmfo.s ⊢ S = N ConstPolyMat R
2 m2cpmfo.t ⊢ T = N matToPolyMat R
3 m2cpmfo.a ⊢ A = N Mat R
4 m2cpmfo.k ⊢ K = Base A
5 m2cpmrngiso.p ⊢ P = Poly 1 ⁡ R
6 m2cpmrngiso.c ⊢ C = N Mat P
7 m2cpmrngiso.u ⊢ U = C ↾ 𝑠 S
8 1 2 3 4 5 6 7 m2cpmrhm ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A RingHom U
9 crngring ⊢ R ∈ CRing → R ∈ Ring
10 9 anim2i ⊢ N ∈ Fin ∧ R ∈ CRing → N ∈ Fin ∧ R ∈ Ring
11 1 2 3 4 m2cpmf1o ⊢ N ∈ Fin ∧ R ∈ Ring → T : K ⟶ 1-1 onto S
12 eqid ⊢ Base C = Base C
13 1 5 6 12 cpmatpmat ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ S → m ∈ Base C
14 13 3expia ⊢ N ∈ Fin ∧ R ∈ Ring → m ∈ S → m ∈ Base C
15 14 ssrdv ⊢ N ∈ Fin ∧ R ∈ Ring → S ⊆ Base C
16 7 12 ressbas2 ⊢ S ⊆ Base C → S = Base U
17 15 16 syl ⊢ N ∈ Fin ∧ R ∈ Ring → S = Base U
18 17 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring → Base U = S
19 18 f1oeq3d ⊢ N ∈ Fin ∧ R ∈ Ring → T : K ⟶ 1-1 onto Base U ↔ T : K ⟶ 1-1 onto S
20 11 19 mpbird ⊢ N ∈ Fin ∧ R ∈ Ring → T : K ⟶ 1-1 onto Base U
21 10 20 syl ⊢ N ∈ Fin ∧ R ∈ CRing → T : K ⟶ 1-1 onto Base U
22 3 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
23 10 22 syl ⊢ N ∈ Fin ∧ R ∈ CRing → A ∈ Ring
24 1 5 6 cpmatsubgpmat ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubGrp ⁡ C
25 7 subggrp ⊢ S ∈ SubGrp ⁡ C → U ∈ Grp
26 10 24 25 3syl ⊢ N ∈ Fin ∧ R ∈ CRing → U ∈ Grp
27 eqid ⊢ Base U = Base U
28 4 27 isrim ⊢ A ∈ Ring ∧ U ∈ Grp → T ∈ A RingIso U ↔ T ∈ A RingHom U ∧ T : K ⟶ 1-1 onto Base U
29 23 26 28 syl2anc ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A RingIso U ↔ T ∈ A RingHom U ∧ T : K ⟶ 1-1 onto Base U
30 8 21 29 mpbir2and ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A RingIso U