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 = ( Poly1 ` R )
m2cpmrngiso.c
|- C = ( N Mat P )
m2cpmrngiso.u
|- U = ( C |`s S )
Assertion m2cpmrngiso
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( 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 = ( Poly1 ` R )
6 m2cpmrngiso.c
 |-  C = ( N Mat P )
7 m2cpmrngiso.u
 |-  U = ( C |`s S )
8 1 2 3 4 5 6 7 m2cpmrhm
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom U ) )
9 crngring
 |-  ( R e. CRing -> R e. Ring )
10 1 2 3 4 m2cpmf1o
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> S )
11 eqid
 |-  ( Base ` C ) = ( Base ` C )
12 1 5 6 11 cpmatpmat
 |-  ( ( N e. Fin /\ R e. Ring /\ m e. S ) -> m e. ( Base ` C ) )
13 12 3expia
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( m e. S -> m e. ( Base ` C ) ) )
14 13 ssrdv
 |-  ( ( N e. Fin /\ R e. Ring ) -> S C_ ( Base ` C ) )
15 7 11 ressbas2
 |-  ( S C_ ( Base ` C ) -> S = ( Base ` U ) )
16 14 15 syl
 |-  ( ( N e. Fin /\ R e. Ring ) -> S = ( Base ` U ) )
17 16 eqcomd
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` U ) = S )
18 17 f1oeq3d
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T : K -1-1-onto-> ( Base ` U ) <-> T : K -1-1-onto-> S ) )
19 10 18 mpbird
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> ( Base ` U ) )
20 9 19 sylan2
 |-  ( ( N e. Fin /\ R e. CRing ) -> T : K -1-1-onto-> ( Base ` U ) )
21 eqid
 |-  ( Base ` U ) = ( Base ` U )
22 4 21 isrim
 |-  ( T e. ( A RingIso U ) <-> ( T e. ( A RingHom U ) /\ T : K -1-1-onto-> ( Base ` U ) ) )
23 8 20 22 sylanbrc
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingIso U ) )