Metamath Proof Explorer


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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 )