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