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	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	asclfval.o	$⊢ \underset{˙}{1} = 1_{W}$
Assertion	asclval	$⊢ X \in K \to A (X) = X \underset{˙}{\cdot} \underset{˙}{1}$

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	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		asclfval.o	$⊢ \underset{˙}{1} = 1_{W}$
6		oveq1	$⊢ x = X \to x \underset{˙}{\cdot} \underset{˙}{1} = X \underset{˙}{\cdot} \underset{˙}{1}$
7	1 2 3 4 5	asclfval	$⊢ A = (x \in K ⟼ x \underset{˙}{\cdot} \underset{˙}{1})$
8		ovex	$⊢ X \underset{˙}{\cdot} \underset{˙}{1} \in V$
9	6 7 8	fvmpt	$⊢ X \in K \to A (X) = X \underset{˙}{\cdot} \underset{˙}{1}$

Metamath Proof Explorer