Theorem scmatric

Description: A ring is isomorphic to every ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019)

	Ref	Expression
Hypotheses	scmatric.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatric.c	⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
	scmatric.s	⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
Assertion	scmatric	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝑅 ≃𝑟 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		scmatric.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatric.c	⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
3		scmatric.s	⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
6		eqid	⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
7		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
8	4 1 5 6 7 2 3	scmatrngiso	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ ( 𝑅 RingIso 𝑆 ) )
9	8	ne0d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
10		brric	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
11	9 10	sylibr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring ) → 𝑅 ≃𝑟 𝑆 )