Theorem scafeq

Description: If the scalar multiplication operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	scaffval.b	$$⊢B={\mathrm{Base}}_W$$
	scaffval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	scaffval.k	$$⊢K={\mathrm{Base}}_F$$
	scaffval.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
	scaffval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
Assertion	scafeq	$$⊢\underset{\dot{}}{·}Fn\left(K\times B\right)\to \underset{\dot{}}{\bullet }=\underset{\dot{}}{·}$$

Proof

Step	Hyp	Ref	Expression
1		scaffval.b	$$⊢B={\mathrm{Base}}_W$$
2		scaffval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		scaffval.k	$$⊢K={\mathrm{Base}}_F$$
4		scaffval.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
5		scaffval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6	1 2 3 4 5	scaffval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$
7		fnov	$$⊢\underset{\dot{}}{·}Fn\left(K\times B\right)\leftrightarrow \underset{\dot{}}{·}=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$
8	7	biimpi	$$⊢\underset{\dot{}}{·}Fn\left(K\times B\right)\to \underset{\dot{}}{·}=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$
9	6 8	eqtr4id	$$⊢\underset{\dot{}}{·}Fn\left(K\times B\right)\to \underset{\dot{}}{\bullet }=\underset{\dot{}}{·}$$