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