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 eqid
 |-  ( Base ` S ) = ( Base ` S )
16 1 15 isrim
 |-  ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ F : K -1-1-onto-> ( Base ` S ) ) )
17 9 14 16 sylanbrc
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F e. ( R RingIso S ) )