Metamath Proof Explorer

Theorem frlmvscafval

Description: Scalar multiplication in a free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses frlmvscafval.y 
|- Y = ( R freeLMod I )
frlmvscafval.b 
|- B = ( Base ` Y )
frlmvscafval.k 
|- K = ( Base ` R )
frlmvscafval.i 
|- ( ph -> I e. W )
frlmvscafval.a 
|- ( ph -> A e. K )
frlmvscafval.x 
|- ( ph -> X e. B )
frlmvscafval.v 
|- .xb = ( .s ` Y )
frlmvscafval.t 
|- .x. = ( .r ` R )
Assertion frlmvscafval 
|- ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) )

Proof

Step Hyp Ref Expression
1 frlmvscafval.y 
 |-  Y = ( R freeLMod I )
2 frlmvscafval.b 
 |-  B = ( Base ` Y )
3 frlmvscafval.k 
 |-  K = ( Base ` R )
4 frlmvscafval.i 
 |-  ( ph -> I e. W )
5 frlmvscafval.a 
 |-  ( ph -> A e. K )
6 frlmvscafval.x 
 |-  ( ph -> X e. B )
7 frlmvscafval.v 
 |-  .xb = ( .s ` Y )
8 frlmvscafval.t 
 |-  .x. = ( .r ` R )
9 1 2 frlmrcl 
 |-  ( X e. B -> R e. _V )
10 6 9 syl 
 |-  ( ph -> R e. _V )
11 1 2 frlmpws 
 |-  ( ( R e. _V /\ I e. W ) -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s B ) )
12 10 4 11 syl2anc 
 |-  ( ph -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s B ) )
13 12 fveq2d 
 |-  ( ph -> ( .s ` Y ) = ( .s ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
14 2 fvexi 
 |-  B e. _V
15 eqid 
 |-  ( ( ( ringLMod ` R ) ^s I ) |`s B ) = ( ( ( ringLMod ` R ) ^s I ) |`s B )
16 eqid 
 |-  ( .s ` ( ( ringLMod ` R ) ^s I ) ) = ( .s ` ( ( ringLMod ` R ) ^s I ) )
17 15 16 ressvsca 
 |-  ( B e. _V -> ( .s ` ( ( ringLMod ` R ) ^s I ) ) = ( .s ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
18 14 17 ax-mp 
 |-  ( .s ` ( ( ringLMod ` R ) ^s I ) ) = ( .s ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) )
19 13 7 18 3eqtr4g 
 |-  ( ph -> .xb = ( .s ` ( ( ringLMod ` R ) ^s I ) ) )
20 19 oveqd 
 |-  ( ph -> ( A .xb X ) = ( A ( .s ` ( ( ringLMod ` R ) ^s I ) ) X ) )
21 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
22 eqid 
 |-  ( Base ` ( ( ringLMod ` R ) ^s I ) ) = ( Base ` ( ( ringLMod ` R ) ^s I ) )
23 rlmvsca 
 |-  ( .r ` R ) = ( .s ` ( ringLMod ` R ) )
24 8 23 eqtri 
 |-  .x. = ( .s ` ( ringLMod ` R ) )
25 eqid 
 |-  ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
26 eqid 
 |-  ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) )
27 fvexd 
 |-  ( ph -> ( ringLMod ` R ) e. _V )
28 rlmsca 
 |-  ( R e. _V -> R = ( Scalar ` ( ringLMod ` R ) ) )
29 10 28 syl 
 |-  ( ph -> R = ( Scalar ` ( ringLMod ` R ) ) )
30 29 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
31 3 30 syl5eq 
 |-  ( ph -> K = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
32 5 31 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
33 12 fveq2d 
 |-  ( ph -> ( Base ` Y ) = ( Base ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
34 2 33 syl5eq 
 |-  ( ph -> B = ( Base ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
35 15 22 ressbasss 
 |-  ( Base ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) C_ ( Base ` ( ( ringLMod ` R ) ^s I ) )
36 34 35 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
37 36 6 sseldd 
 |-  ( ph -> X e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
38 21 22 24 16 25 26 27 4 32 37 pwsvscafval 
 |-  ( ph -> ( A ( .s ` ( ( ringLMod ` R ) ^s I ) ) X ) = ( ( I X. { A } ) oF .x. X ) )
39 20 38 eqtrd 
 |-  ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) )