Theorem scmatf

Description: There is a function from a ring to any ring of scalar matrices over this ring. (Contributed by AV, 25-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 )
Assertion	scmatf	|- ( ( N e. Fin /\ R e. Ring ) -> F : K --> C )

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		eqid	|- ( Base ` A ) = ( Base ` A )
8		eqid	|- ( 0g ` R ) = ( 0g ` R )
9	2 7 1 8 6	scmatid	|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. C )
10	3 9	eqeltrid	|- ( ( N e. Fin /\ R e. Ring ) -> .1. e. C )
11	10	anim1ci	|- ( ( ( N e. Fin /\ R e. Ring ) /\ x e. K ) -> ( x e. K /\ .1. e. C ) )
12	1 2 6 4	smatvscl	|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. K /\ .1. e. C ) ) -> ( x .* .1. ) e. C )
13	11 12	syldan	|- ( ( ( N e. Fin /\ R e. Ring ) /\ x e. K ) -> ( x .* .1. ) e. C )
14	13 5	fmptd	|- ( ( N e. Fin /\ R e. Ring ) -> F : K --> C )