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