Theorem scmatrhmval

Description: The value of the ring homomorphism F . (Contributed by AV, 22-Dec-2019)

	Ref	Expression
Hypotheses	scmatrhmval.k	$$⊢K={\mathrm{Base}}_R$$
	scmatrhmval.a	$$⊢A=N\mathrm{Mat}R$$
	scmatrhmval.o	$$⊢\underset{\dot{}}{1}=1_A$$
	scmatrhmval.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
	scmatrhmval.f	$$⊢F=\left(x\in K⟼x\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
Assertion	scmatrhmval	$$⊢\left(R\in V\wedge X\in K\right)\to F\left(X\right)=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		scmatrhmval.k	$$⊢K={\mathrm{Base}}_R$$
2		scmatrhmval.a	$$⊢A=N\mathrm{Mat}R$$
3		scmatrhmval.o	$$⊢\underset{\dot{}}{1}=1_A$$
4		scmatrhmval.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
5		scmatrhmval.f	$$⊢F=\left(x\in K⟼x\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
6		oveq1	$$⊢x=X\to x\underset{\dot{}}{\ast }\underset{\dot{}}{1}=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
7		simpr	$$⊢\left(R\in V\wedge X\in K\right)\to X\in K$$
8		ovexd	$$⊢\left(R\in V\wedge X\in K\right)\to X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in \mathrm{V}$$
9	5 6 7 8	fvmptd3	$$⊢\left(R\in V\wedge X\in K\right)\to F\left(X\right)=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$