Theorem asclval

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

	Ref	Expression
Hypotheses	asclfval.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	asclfval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	asclfval.k	$$⊢K={\mathrm{Base}}_F$$
	asclfval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	asclfval.o	$$⊢\underset{\dot{}}{1}=1_W$$
Assertion	asclval	$$⊢X\in K\to A\left(X\right)=X\underset{\dot{}}{·}\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		asclfval.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclfval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		asclfval.k	$$⊢K={\mathrm{Base}}_F$$
4		asclfval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		asclfval.o	$$⊢\underset{\dot{}}{1}=1_W$$
6		oveq1	$$⊢x=X\to x\underset{\dot{}}{·}\underset{\dot{}}{1}=X\underset{\dot{}}{·}\underset{\dot{}}{1}$$
7	1 2 3 4 5	asclfval	$$⊢A=\left(x\in K⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
8		ovex	$$⊢X\underset{\dot{}}{·}\underset{\dot{}}{1}\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢X\in K\to A\left(X\right)=X\underset{\dot{}}{·}\underset{\dot{}}{1}$$