Metamath Proof Explorer

Theorem imasvscaval

Description: The value of an image structure's scalar multiplication. (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 ) ) ) )
Assertion imasvscaval 
|- ( ( ph /\ X e. K /\ Y e. V ) -> ( X .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )

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 1 2 3 4 5 6 7 8 9 imasvscafn 
 |-  ( ph -> .xb Fn ( K X. B ) )
11 fnfun 
 |-  ( .xb Fn ( K X. B ) -> Fun .xb )
12 10 11 syl 
 |-  ( ph -> Fun .xb )
13 12 3ad2ant1 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> Fun .xb )
14 eqidd 
 |-  ( q = Y -> K = K )
15 fveq2 
 |-  ( q = Y -> ( F ` q ) = ( F ` Y ) )
16 15 sneqd 
 |-  ( q = Y -> { ( F ` q ) } = { ( F ` Y ) } )
17 oveq2 
 |-  ( q = Y -> ( p .x. q ) = ( p .x. Y ) )
18 17 fveq2d 
 |-  ( q = Y -> ( F ` ( p .x. q ) ) = ( F ` ( p .x. Y ) ) )
19 14 16 18 mpoeq123dv 
 |-  ( q = Y -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) )
20 19 ssiun2s 
 |-  ( Y e. V -> ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) C_ U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
21 20 3ad2ant3 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) C_ U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
22 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 ) ) ) )
23 22 3ad2ant1 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> .xb = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
24 21 23 sseqtrrd 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) C_ .xb )
25 simp2 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> X e. K )
26 fvex 
 |-  ( F ` Y ) e. _V
27 26 snid 
 |-  ( F ` Y ) e. { ( F ` Y ) }
28 opelxpi 
 |-  ( ( X e. K /\ ( F ` Y ) e. { ( F ` Y ) } ) -> <. X , ( F ` Y ) >. e. ( K X. { ( F ` Y ) } ) )
29 25 27 28 sylancl 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> <. X , ( F ` Y ) >. e. ( K X. { ( F ` Y ) } ) )
30 eqid 
 |-  ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) = ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) )
31 fvex 
 |-  ( F ` ( p .x. Y ) ) e. _V
32 30 31 dmmpo 
 |-  dom ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) = ( K X. { ( F ` Y ) } )
33 29 32 eleqtrrdi 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> <. X , ( F ` Y ) >. e. dom ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) )
34 funssfv 
 |-  ( ( Fun .xb /\ ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) C_ .xb /\ <. X , ( F ` Y ) >. e. dom ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) ) -> ( .xb ` <. X , ( F ` Y ) >. ) = ( ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) ` <. X , ( F ` Y ) >. ) )
35 13 24 33 34 syl3anc 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> ( .xb ` <. X , ( F ` Y ) >. ) = ( ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) ` <. X , ( F ` Y ) >. ) )
36 df-ov 
 |-  ( X .xb ( F ` Y ) ) = ( .xb ` <. X , ( F ` Y ) >. )
37 df-ov 
 |-  ( X ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) ( F ` Y ) ) = ( ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) ` <. X , ( F ` Y ) >. )
38 35 36 37 3eqtr4g 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> ( X .xb ( F ` Y ) ) = ( X ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) ( F ` Y ) ) )
39 fvoveq1 
 |-  ( p = X -> ( F ` ( p .x. Y ) ) = ( F ` ( X .x. Y ) ) )
40 eqidd 
 |-  ( x = ( F ` Y ) -> ( F ` ( X .x. Y ) ) = ( F ` ( X .x. Y ) ) )
41 fvex 
 |-  ( F ` ( X .x. Y ) ) e. _V
42 39 40 30 41 ovmpo 
 |-  ( ( X e. K /\ ( F ` Y ) e. { ( F ` Y ) } ) -> ( X ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
43 25 27 42 sylancl 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> ( X ( p e. K , x e. { ( F ` Y ) } |-> ( F ` ( p .x. Y ) ) ) ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
44 38 43 eqtrd 
 |-  ( ( ph /\ X e. K /\ Y e. V ) -> ( X .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )