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 1 2 3 4 m2cpmf1o ⊢ N ∈ Fin ∧ R ∈ Ring → T : K ⟶ 1-1 onto S
11 eqid ⊢ Base C = Base C
12 1 5 6 11 cpmatpmat ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ S → m ∈ Base C
13 12 3expia ⊢ N ∈ Fin ∧ R ∈ Ring → m ∈ S → m ∈ Base C
14 13 ssrdv ⊢ N ∈ Fin ∧ R ∈ Ring → S ⊆ Base C
15 7 11 ressbas2 ⊢ S ⊆ Base C → S = Base U
16 14 15 syl ⊢ N ∈ Fin ∧ R ∈ Ring → S = Base U
17 16 eqcomd ⊢ N ∈ Fin ∧ R ∈ Ring → Base U = S
18 17 f1oeq3d ⊢ N ∈ Fin ∧ R ∈ Ring → T : K ⟶ 1-1 onto Base U ↔ T : K ⟶ 1-1 onto S
19 10 18 mpbird ⊢ N ∈ Fin ∧ R ∈ Ring → T : K ⟶ 1-1 onto Base U
20 9 19 sylan2 ⊢ N ∈ Fin ∧ R ∈ CRing → T : K ⟶ 1-1 onto Base U
21 eqid ⊢ Base U = Base U
22 4 21 isrim ⊢ T ∈ A RingIso U ↔ T ∈ A RingHom U ∧ T : K ⟶ 1-1 onto Base U
23 8 20 22 sylanbrc ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ A RingIso U