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={\mathrm{Base}}_R$$
	scmatrhmval.a	$$⊢A=N\mathrm{Mat}R$$
	scmatrhmval.o	$$⊢\underset{\dot{}}{1}=1_A$$
	scmatrhmval.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
	scmatrhmval.f	$$⊢F=\left(x\in K⟼x\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
	scmatrhmval.c	$$⊢C=N\mathrm{ScMat}R$$
Assertion	scmatf1o	$$⊢\left(N\in \mathrm{Fin}\wedge N\ne \varnothing \wedge R\in \mathrm{Ring}\right)\to F:K\underset{1-1\; onto}{⟶}C$$

Proof

Step	Hyp	Ref	Expression
1		scmatrhmval.k	$$⊢K={\mathrm{Base}}_R$$
2		scmatrhmval.a	$$⊢A=N\mathrm{Mat}R$$
3		scmatrhmval.o	$$⊢\underset{\dot{}}{1}=1_A$$
4		scmatrhmval.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
5		scmatrhmval.f	$$⊢F=\left(x\in K⟼x\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
6		scmatrhmval.c	$$⊢C=N\mathrm{ScMat}R$$
7	1 2 3 4 5 6	scmatf1	$$⊢\left(N\in \mathrm{Fin}\wedge N\ne \varnothing \wedge R\in \mathrm{Ring}\right)\to F:K\underset{1-1}{⟶}C$$
8	1 2 3 4 5 6	scmatfo	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to F:K\underset{onto}{⟶}C$$
9	8	3adant2	$$⊢\left(N\in \mathrm{Fin}\wedge N\ne \varnothing \wedge R\in \mathrm{Ring}\right)\to F:K\underset{onto}{⟶}C$$
10		df-f1o	$$⊢F:K\underset{1-1\; onto}{⟶}C\leftrightarrow \left(F:K\underset{1-1}{⟶}C\wedge F:K\underset{onto}{⟶}C\right)$$
11	7 9 10	sylanbrc	$$⊢\left(N\in \mathrm{Fin}\wedge N\ne \varnothing \wedge R\in \mathrm{Ring}\right)\to F:K\underset{1-1\; onto}{⟶}C$$