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	⊢ 𝐾 = ( Base ‘ 𝑅 )
	scmatrhmval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatrhmval.o	⊢ 1 = ( 1r ‘ 𝐴 )
	scmatrhmval.t	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	scmatrhmval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
	scmatrhmval.c	⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
Assertion	scmatf1o	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1-onto→ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		scmatrhmval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
2		scmatrhmval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		scmatrhmval.o	⊢ 1 = ( 1r ‘ 𝐴 )
4		scmatrhmval.t	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
5		scmatrhmval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
6		scmatrhmval.c	⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
7	1 2 3 4 5 6	scmatf1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1→ 𝐶 )
8	1 2 3 4 5 6	scmatfo	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –onto→ 𝐶 )
9	8	3adant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –onto→ 𝐶 )
10		df-f1o	⊢ ( 𝐹 : 𝐾 –1-1-onto→ 𝐶 ↔ ( 𝐹 : 𝐾 –1-1→ 𝐶 ∧ 𝐹 : 𝐾 –onto→ 𝐶 ) )
11	7 9 10	sylanbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1-onto→ 𝐶 )