Theorem scmatf1o

Description: There is a bijection between a ring and any ring of scalar matrices with positive dimension over this ring. (Contributed by AV, 26-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 )
Assertion	scmatf1o	|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-onto-> C )

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	1 2 3 4 5 6	scmatf1	|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-> C )
8	1 2 3 4 5 6	scmatfo	|- ( ( N e. Fin /\ R e. Ring ) -> F : K -onto-> C )
9	8	3adant2	|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -onto-> C )
10		df-f1o	|- ( F : K -1-1-onto-> C <-> ( F : K -1-1-> C /\ F : K -onto-> C ) )
11	7 9 10	sylanbrc	|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-onto-> C )