Theorem scmatrhm

Description: There is a ring homomorphism from a ring to the ring of scalar matrices over this ring. (Contributed by AV, 29-Dec-2019)

	Ref	Expression
Hypotheses	scmatrhmval.k	|- K = ( Base ` R )
	scmatrhmval.a	|- A = ( N Mat R )
	scmatrhmval.o	|- .1. = ( 1r ` A )
	scmatrhmval.t	|- .* = ( .s ` A )
	scmatrhmval.f	|- F = ( x e. K |-> ( x .* .1. ) )
	scmatrhmval.c	|- C = ( N ScMat R )
	scmatghm.s	|- S = ( A |`s C )
Assertion	scmatrhm	|- ( ( N e. Fin /\ R e. Ring ) -> F e. ( R RingHom S ) )

Proof

Step	Hyp	Ref	Expression
1		scmatrhmval.k	|- K = ( Base ` R )
2		scmatrhmval.a	|- A = ( N Mat R )
3		scmatrhmval.o	|- .1. = ( 1r ` A )
4		scmatrhmval.t	|- .* = ( .s ` A )
5		scmatrhmval.f	|- F = ( x e. K |-> ( x .* .1. ) )
6		scmatrhmval.c	|- C = ( N ScMat R )
7		scmatghm.s	|- S = ( A |`s C )
8		simpr	|- ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
9		eqid	|- ( Base ` A ) = ( Base ` A )
10		eqid	|- ( 0g ` R ) = ( 0g ` R )
11	2 9 1 10 6	scmatsrng	|- ( ( N e. Fin /\ R e. Ring ) -> C e. ( SubRing ` A ) )
12	7	subrgring	|- ( C e. ( SubRing ` A ) -> S e. Ring )
13	11 12	syl	|- ( ( N e. Fin /\ R e. Ring ) -> S e. Ring )
14	1 2 3 4 5 6 7	scmatghm	|- ( ( N e. Fin /\ R e. Ring ) -> F e. ( R GrpHom S ) )
15		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
16		eqid	|- ( mulGrp ` S ) = ( mulGrp ` S )
17	1 2 3 4 5 6 7 15 16	scmatmhm	|- ( ( N e. Fin /\ R e. Ring ) -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
18	14 17	jca	|- ( ( N e. Fin /\ R e. Ring ) -> ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )
19	15 16	isrhm	|- ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) ) )
20	8 13 18 19	syl21anbrc	|- ( ( N e. Fin /\ R e. Ring ) -> F e. ( R RingHom S ) )