This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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