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 = ( Base ` W )
	scaffval.f	|- F = ( Scalar ` W )
	scaffval.k	|- K = ( Base ` F )
	scaffval.a	|- .xb = ( .sf ` W )
	scaffval.s	|- .x. = ( .s ` W )
Assertion	scafeq	|- ( .x. Fn ( K X. B ) -> .xb = .x. )

Proof

Step	Hyp	Ref	Expression
1		scaffval.b	|- B = ( Base ` W )
2		scaffval.f	|- F = ( Scalar ` W )
3		scaffval.k	|- K = ( Base ` F )
4		scaffval.a	|- .xb = ( .sf ` W )
5		scaffval.s	|- .x. = ( .s ` W )
6	1 2 3 4 5	scaffval	|- .xb = ( x e. K , y e. B |-> ( x .x. y ) )
7		fnov	|- ( .x. Fn ( K X. B ) <-> .x. = ( x e. K , y e. B |-> ( x .x. y ) ) )
8	7	biimpi	|- ( .x. Fn ( K X. B ) -> .x. = ( x e. K , y e. B |-> ( x .x. y ) ) )
9	6 8	eqtr4id	|- ( .x. Fn ( K X. B ) -> .xb = .x. )