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	|- A = ( N Mat R )
	scmatric.c	|- C = ( N ScMat R )
	scmatric.s	|- S = ( A |`s C )
Assertion	scmatric	|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> R ~=r S )

Proof

Step	Hyp	Ref	Expression
1		scmatric.a	|- A = ( N Mat R )
2		scmatric.c	|- C = ( N ScMat R )
3		scmatric.s	|- S = ( A |`s C )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5		eqid	|- ( 1r ` A ) = ( 1r ` A )
6		eqid	|- ( .s ` A ) = ( .s ` A )
7		eqid	|- ( x e. ( Base ` R ) |-> ( x ( .s ` A ) ( 1r ` A ) ) ) = ( x e. ( Base ` R ) |-> ( x ( .s ` A ) ( 1r ` A ) ) )
8	4 1 5 6 7 2 3	scmatrngiso	|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> ( x e. ( Base ` R ) |-> ( x ( .s ` A ) ( 1r ` A ) ) ) e. ( R RingIso S ) )
9	8	ne0d	|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> ( R RingIso S ) =/= (/) )
10		brric	|- ( R ~=r S <-> ( R RingIso S ) =/= (/) )
11	9 10	sylibr	|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> R ~=r S )