Theorem scmatrhmval

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

	Ref	Expression
Hypotheses	scmatrhmval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	scmatrhmval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatrhmval.o	⊢ 1 = ( 1r ‘ 𝐴 )
	scmatrhmval.t	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	scmatrhmval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
Assertion	scmatrhmval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ∗ 1 ) )

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		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∗ 1 ) = ( 𝑋 ∗ 1 ) )
7		simpr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
8		ovexd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ∗ 1 ) ∈ V )
9	5 6 7 8	fvmptd3	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ∗ 1 ) )