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

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		scmatghm.s	⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
8	1 2 3 4 5 6 7	scmatrhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
9	8	3adant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
10	1 2 3 4 5 6	scmatf1o	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1-onto→ 𝐶 )
11	2 6 7	scmatstrbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑆 ) = 𝐶 )
12	11	3adant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑆 ) = 𝐶 )
13	12	f1oeq3d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( 𝐹 : 𝐾 –1-1-onto→ ( Base ‘ 𝑆 ) ↔ 𝐹 : 𝐾 –1-1-onto→ 𝐶 ) )
14	10 13	mpbird	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –1-1-onto→ ( Base ‘ 𝑆 ) )
15		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
16	1 15	isrim	⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐹 : 𝐾 –1-1-onto→ ( Base ‘ 𝑆 ) ) )
17	9 14 16	sylanbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) )