Theorem imasvscaf

Description: The image structure's scalar multiplication is closed in the base set. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	imasvscaf.u	|- ( ph -> U = ( F "s R ) )
	imasvscaf.v	|- ( ph -> V = ( Base ` R ) )
	imasvscaf.f	|- ( ph -> F : V -onto-> B )
	imasvscaf.r	|- ( ph -> R e. Z )
	imasvscaf.g	|- G = ( Scalar ` R )
	imasvscaf.k	|- K = ( Base ` G )
	imasvscaf.q	|- .x. = ( .s ` R )
	imasvscaf.s	|- .xb = ( .s ` U )
	imasvscaf.e	|- ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )
	imasvscaf.c	|- ( ( ph /\ ( p e. K /\ q e. V ) ) -> ( p .x. q ) e. V )
Assertion	imasvscaf	|- ( ph -> .xb : ( K X. B ) --> B )

Proof

Step	Hyp	Ref	Expression
1		imasvscaf.u	|- ( ph -> U = ( F "s R ) )
2		imasvscaf.v	|- ( ph -> V = ( Base ` R ) )
3		imasvscaf.f	|- ( ph -> F : V -onto-> B )
4		imasvscaf.r	|- ( ph -> R e. Z )
5		imasvscaf.g	|- G = ( Scalar ` R )
6		imasvscaf.k	|- K = ( Base ` G )
7		imasvscaf.q	|- .x. = ( .s ` R )
8		imasvscaf.s	|- .xb = ( .s ` U )
9		imasvscaf.e	|- ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )
10		imasvscaf.c	|- ( ( ph /\ ( p e. K /\ q e. V ) ) -> ( p .x. q ) e. V )
11	1 2 3 4 5 6 7 8 9	imasvscafn	|- ( ph -> .xb Fn ( K X. B ) )
12	1 2 3 4 5 6 7 8	imasvsca	|- ( ph -> .xb = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
13		fof	|- ( F : V -onto-> B -> F : V --> B )
14	3 13	syl	|- ( ph -> F : V --> B )
15	14	ffvelcdmda	|- ( ( ph /\ ( p .x. q ) e. V ) -> ( F ` ( p .x. q ) ) e. B )
16	10 15	syldan	|- ( ( ph /\ ( p e. K /\ q e. V ) ) -> ( F ` ( p .x. q ) ) e. B )
17	16	ralrimivw	|- ( ( ph /\ ( p e. K /\ q e. V ) ) -> A. x e. { ( F ` q ) } ( F ` ( p .x. q ) ) e. B )
18	17	anass1rs	|- ( ( ( ph /\ q e. V ) /\ p e. K ) -> A. x e. { ( F ` q ) } ( F ` ( p .x. q ) ) e. B )
19	18	ralrimiva	|- ( ( ph /\ q e. V ) -> A. p e. K A. x e. { ( F ` q ) } ( F ` ( p .x. q ) ) e. B )
20		eqid	|- ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
21	20	fmpo	|- ( A. p e. K A. x e. { ( F ` q ) } ( F ` ( p .x. q ) ) e. B <-> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> B )
22	19 21	sylib	|- ( ( ph /\ q e. V ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> B )
23		fssxp	|- ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> B -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. { ( F ` q ) } ) X. B ) )
24	22 23	syl	|- ( ( ph /\ q e. V ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. { ( F ` q ) } ) X. B ) )
25	14	ffvelcdmda	|- ( ( ph /\ q e. V ) -> ( F ` q ) e. B )
26	25	snssd	|- ( ( ph /\ q e. V ) -> { ( F ` q ) } C_ B )
27		xpss2	|- ( { ( F ` q ) } C_ B -> ( K X. { ( F ` q ) } ) C_ ( K X. B ) )
28		xpss1	|- ( ( K X. { ( F ` q ) } ) C_ ( K X. B ) -> ( ( K X. { ( F ` q ) } ) X. B ) C_ ( ( K X. B ) X. B ) )
29	26 27 28	3syl	|- ( ( ph /\ q e. V ) -> ( ( K X. { ( F ` q ) } ) X. B ) C_ ( ( K X. B ) X. B ) )
30	24 29	sstrd	|- ( ( ph /\ q e. V ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. B ) )
31	30	ralrimiva	|- ( ph -> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. B ) )
32		iunss	|- ( U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. B ) <-> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. B ) )
33	31 32	sylibr	|- ( ph -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. B ) )
34	12 33	eqsstrd	|- ( ph -> .xb C_ ( ( K X. B ) X. B ) )
35		dff2	|- ( .xb : ( K X. B ) --> B <-> ( .xb Fn ( K X. B ) /\ .xb C_ ( ( K X. B ) X. B ) ) )
36	11 34 35	sylanbrc	|- ( ph -> .xb : ( K X. B ) --> B )