Theorem lmodscaf

Description: The scalar multiplication operation is a function. (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 )
Assertion	lmodscaf	|- ( W e. LMod -> .xb : ( K X. B ) --> B )

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		eqid	|- ( .s ` W ) = ( .s ` W )
6	1 2 5 3	lmodvscl	|- ( ( W e. LMod /\ x e. K /\ y e. B ) -> ( x ( .s ` W ) y ) e. B )
7	6	3expb	|- ( ( W e. LMod /\ ( x e. K /\ y e. B ) ) -> ( x ( .s ` W ) y ) e. B )
8	7	ralrimivva	|- ( W e. LMod -> A. x e. K A. y e. B ( x ( .s ` W ) y ) e. B )
9	1 2 3 4 5	scaffval	|- .xb = ( x e. K , y e. B |-> ( x ( .s ` W ) y ) )
10	9	fmpo	|- ( A. x e. K A. y e. B ( x ( .s ` W ) y ) e. B <-> .xb : ( K X. B ) --> B )
11	8 10	sylib	|- ( W e. LMod -> .xb : ( K X. B ) --> B )