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	$⊢ \underset{˙}{1} = 1_{A}$
	scmatrhmval.t	$⊢ \underset{˙}{*} = \cdot_{A}$
	scmatrhmval.f	$⊢ F = (x \in K ⟼ x \underset{˙}{*} \underset{˙}{1})$
	scmatrhmval.c	$⊢ C = N ScMat R$
	scmatghm.s	$⊢ S = A ↾_{𝑠} C$
Assertion	scmatrhm	$⊢ (N \in Fin \land R \in Ring) \to F \in (R RingHom S)$

Step	Hyp	Ref	Expression
1		scmatrhmval.k	$⊢ K = {Base}_{R}$
2		scmatrhmval.a	$⊢ A = N Mat R$
3		scmatrhmval.o	$⊢ \underset{˙}{1} = 1_{A}$
4		scmatrhmval.t	$⊢ \underset{˙}{*} = \cdot_{A}$
5		scmatrhmval.f	$⊢ F = (x \in K ⟼ x \underset{˙}{*} \underset{˙}{1})$
6		scmatrhmval.c	$⊢ C = N ScMat R$
7		scmatghm.s	$⊢ S = A ↾_{𝑠} C$
8		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
9		eqid	$⊢ {Base}_{A} = {Base}_{A}$
10		eqid	$⊢ 0_{R} = 0_{R}$
11	2 9 1 10 6	scmatsrng	$⊢ (N \in Fin \land R \in Ring) \to C \in SubRing (A)$
12	7	subrgring	$⊢ C \in SubRing (A) \to S \in Ring$
13	11 12	syl	$⊢ (N \in Fin \land R \in Ring) \to S \in Ring$
14	1 2 3 4 5 6 7	scmatghm	$⊢ (N \in Fin \land R \in Ring) \to F \in (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 \in Fin \land R \in Ring) \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})$
18	14 17	jca	$⊢ (N \in Fin \land R \in Ring) \to (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}))$
19	15 16	isrhm	$⊢ F \in (R RingHom S) \leftrightarrow ((R \in Ring \land S \in Ring) \land (F \in (R GrpHom S) \land F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})))$
20	8 13 18 19	syl21anbrc	$⊢ (N \in Fin \land R \in Ring) \to F \in (R RingHom S)$

Metamath Proof Explorer