Theorem scmatrhmval

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

	Ref	Expression
Hypotheses	scmatrhmval.k	|- K = ( Base ` R )
	scmatrhmval.a	|- A = ( N Mat R )
	scmatrhmval.o	|- .1. = ( 1r ` A )
	scmatrhmval.t	|- .* = ( .s ` A )
	scmatrhmval.f	|- F = ( x e. K |-> ( x .* .1. ) )
Assertion	scmatrhmval	|- ( ( R e. V /\ X e. K ) -> ( F ` X ) = ( X .* .1. ) )

Proof

Step	Hyp	Ref	Expression
1		scmatrhmval.k	|- K = ( Base ` R )
2		scmatrhmval.a	|- A = ( N Mat R )
3		scmatrhmval.o	|- .1. = ( 1r ` A )
4		scmatrhmval.t	|- .* = ( .s ` A )
5		scmatrhmval.f	|- F = ( x e. K |-> ( x .* .1. ) )
6		oveq1	|- ( x = X -> ( x .* .1. ) = ( X .* .1. ) )
7		simpr	|- ( ( R e. V /\ X e. K ) -> X e. K )
8		ovexd	|- ( ( R e. V /\ X e. K ) -> ( X .* .1. ) e. _V )
9	5 6 7 8	fvmptd3	|- ( ( R e. V /\ X e. K ) -> ( F ` X ) = ( X .* .1. ) )