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