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 ) )