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 9 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
11 1 2 3 4 m2cpmf1o 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> S )
12 eqid 
 |-  ( Base ` C ) = ( Base ` C )
13 1 5 6 12 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ m e. S ) -> m e. ( Base ` C ) )
14 13 3expia 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( m e. S -> m e. ( Base ` C ) ) )
15 14 ssrdv 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S C_ ( Base ` C ) )
16 7 12 ressbas2 
 |-  ( S C_ ( Base ` C ) -> S = ( Base ` U ) )
17 15 16 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S = ( Base ` U ) )
18 17 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` U ) = S )
19 18 f1oeq3d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T : K -1-1-onto-> ( Base ` U ) <-> T : K -1-1-onto-> S ) )
20 11 19 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> ( Base ` U ) )
21 10 20 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T : K -1-1-onto-> ( Base ` U ) )
22 3 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
23 10 22 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
24 1 5 6 cpmatsubgpmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )
25 7 subggrp 
 |-  ( S e. ( SubGrp ` C ) -> U e. Grp )
26 10 24 25 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> U e. Grp )
27 eqid 
 |-  ( Base ` U ) = ( Base ` U )
28 4 27 isrim 
 |-  ( ( A e. Ring /\ U e. Grp ) -> ( T e. ( A RingIso U ) <-> ( T e. ( A RingHom U ) /\ T : K -1-1-onto-> ( Base ` U ) ) ) )
29 23 26 28 syl2anc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( T e. ( A RingIso U ) <-> ( T e. ( A RingHom U ) /\ T : K -1-1-onto-> ( Base ` U ) ) ) )
30 8 21 29 mpbir2and 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingIso U ) )