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	⊢ 𝐾 = ( Base ‘ 𝑅 )
	scmatrhmval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatrhmval.o	⊢ 1 = ( 1r ‘ 𝐴 )
	scmatrhmval.t	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	scmatrhmval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
	scmatrhmval.c	⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
Assertion	scmatf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 ⟶ 𝐶 )

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		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
8		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9	2 7 1 8 6	scmatid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐶 )
10	3 9	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ 𝐶 )
11	10	anim1ci	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑥 ∈ 𝐾 ∧ 1 ∈ 𝐶 ) )
12	1 2 6 4	smatvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐾 ∧ 1 ∈ 𝐶 ) ) → ( 𝑥 ∗ 1 ) ∈ 𝐶 )
13	11 12	syldan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑥 ∗ 1 ) ∈ 𝐶 )
14	13 5	fmptd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 ⟶ 𝐶 )