Metamath Proof Explorer

Theorem scmatrngiso

Description: There is a ring isomorphism from a ring to the ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019)

Ref Expression
Hypotheses scmatrhmval.k 
|- K = ( Base ` R )
scmatrhmval.a 
|- A = ( N Mat R )
scmatrhmval.o 
|- .1. = ( 1r ` A )
scmatrhmval.t 
|- .* = ( .s ` A )
scmatrhmval.f 
|- F = ( x e. K |-> ( x .* .1. ) )
scmatrhmval.c 
|- C = ( N ScMat R )
scmatghm.s 
|- S = ( A |`s C )
Assertion scmatrngiso 
|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F e. ( R RingIso S ) )

Proof

Step Hyp Ref Expression
1 scmatrhmval.k 
 |-  K = ( Base ` R )
2 scmatrhmval.a 
 |-  A = ( N Mat R )
3 scmatrhmval.o 
 |-  .1. = ( 1r ` A )
4 scmatrhmval.t 
 |-  .* = ( .s ` A )
5 scmatrhmval.f 
 |-  F = ( x e. K |-> ( x .* .1. ) )
6 scmatrhmval.c 
 |-  C = ( N ScMat R )
7 scmatghm.s 
 |-  S = ( A |`s C )
8 1 2 3 4 5 6 7 scmatrhm 
 |-  ( ( N e. Fin /\ R e. Ring ) -> F e. ( R RingHom S ) )
9 8 3adant2 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F e. ( R RingHom S ) )
10 1 2 3 4 5 6 scmatf1o 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-onto-> C )
11 2 6 7 scmatstrbas 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` S ) = C )
12 11 3adant2 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> ( Base ` S ) = C )
13 12 f1oeq3d 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> ( F : K -1-1-onto-> ( Base ` S ) <-> F : K -1-1-onto-> C ) )
14 10 13 mpbird 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-onto-> ( Base ` S ) )
15 simp3 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> R e. Ring )
16 eqid 
 |-  ( Base ` A ) = ( Base ` A )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 2 16 1 17 6 scmatsrng 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. ( SubRing ` A ) )
19 7 subrgring 
 |-  ( C e. ( SubRing ` A ) -> S e. Ring )
20 18 19 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. Ring )
21 eqid 
 |-  ( Base ` S ) = ( Base ` S )
22 1 21 isrim 
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ F : K -1-1-onto-> ( Base ` S ) ) ) )
23 15 20 22 3imp3i2an 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ F : K -1-1-onto-> ( Base ` S ) ) ) )
24 9 14 23 mpbir2and 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F e. ( R RingIso S ) )