Theorem asclval

Description: Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015)

	Ref	Expression
Hypotheses	asclfval.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	asclfval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	asclfval.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	asclfval.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	asclfval.o	⊢ 1 = ( 1r ‘ 𝑊 )
Assertion	asclval	⊢ ( 𝑋 ∈ 𝐾 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 · 1 ) )

Proof

Step	Hyp	Ref	Expression
1		asclfval.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		asclfval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		asclfval.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
4		asclfval.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		asclfval.o	⊢ 1 = ( 1r ‘ 𝑊 )
6		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 1 ) = ( 𝑋 · 1 ) )
7	1 2 3 4 5	asclfval	⊢ 𝐴 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 1 ) )
8		ovex	⊢ ( 𝑋 · 1 ) ∈ V
9	6 7 8	fvmpt	⊢ ( 𝑋 ∈ 𝐾 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 · 1 ) )