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

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		scmatghm.s	⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
8		simpr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
9		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
10		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
11	2 9 1 10 6	scmatsrng	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ ( SubRing ‘ 𝐴 ) )
12	7	subrgring	⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐴 ) → 𝑆 ∈ Ring )
13	11 12	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ Ring )
14	1 2 3 4 5 6 7	scmatghm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
15		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
16		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
17	1 2 3 4 5 6 7 15 16	scmatmhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) )
18	14 17	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )
19	15 16	isrhm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ) )
20	8 13 18 19	syl21anbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )