scmatf

Description: There is a function from a ring to any ring of scalar matrices over this ring. (Contributed by AV, 25-Dec-2019)

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		eqid	$⊢ {Base}_{A} = {Base}_{A}$
8		eqid	$⊢ 0_{R} = 0_{R}$
9	2 7 1 8 6	scmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in C$
10	3 9	eqeltrid	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} \in C$
11	10	anim1ci	$⊢ ((N \in Fin \land R \in Ring) \land x \in K) \to (x \in K \land \underset{˙}{1} \in C)$
12	1 2 6 4	smatvscl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in K \land \underset{˙}{1} \in C)) \to x \underset{˙}{*} \underset{˙}{1} \in C$
13	11 12	syldan	$⊢ ((N \in Fin \land R \in Ring) \land x \in K) \to x \underset{˙}{*} \underset{˙}{1} \in C$
14	13 5	fmptd	$⊢ (N \in Fin \land R \in Ring) \to F : K ⟶ C$

Metamath Proof Explorer