Theorem asclval

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

	Ref	Expression
Hypotheses	asclfval.a	|- A = ( algSc ` W )
	asclfval.f	|- F = ( Scalar ` W )
	asclfval.k	|- K = ( Base ` F )
	asclfval.s	|- .x. = ( .s ` W )
	asclfval.o	|- .1. = ( 1r ` W )
Assertion	asclval	|- ( X e. K -> ( A ` X ) = ( X .x. .1. ) )

Proof

Step	Hyp	Ref	Expression
1		asclfval.a	|- A = ( algSc ` W )
2		asclfval.f	|- F = ( Scalar ` W )
3		asclfval.k	|- K = ( Base ` F )
4		asclfval.s	|- .x. = ( .s ` W )
5		asclfval.o	|- .1. = ( 1r ` W )
6		oveq1	|- ( x = X -> ( x .x. .1. ) = ( X .x. .1. ) )
7	1 2 3 4 5	asclfval	|- A = ( x e. K |-> ( x .x. .1. ) )
8		ovex	|- ( X .x. .1. ) e. _V
9	6 7 8	fvmpt	|- ( X e. K -> ( A ` X ) = ( X .x. .1. ) )