Step |
Hyp |
Ref |
Expression |
1 |
|
pwsvscaval.y |
|- Y = ( R ^s I ) |
2 |
|
pwsvscaval.b |
|- B = ( Base ` Y ) |
3 |
|
pwsvscaval.s |
|- .x. = ( .s ` R ) |
4 |
|
pwsvscaval.t |
|- .xb = ( .s ` Y ) |
5 |
|
pwsvscaval.f |
|- F = ( Scalar ` R ) |
6 |
|
pwsvscaval.k |
|- K = ( Base ` F ) |
7 |
|
pwsvscaval.r |
|- ( ph -> R e. V ) |
8 |
|
pwsvscaval.i |
|- ( ph -> I e. W ) |
9 |
|
pwsvscaval.a |
|- ( ph -> A e. K ) |
10 |
|
pwsvscaval.x |
|- ( ph -> X e. B ) |
11 |
1 5
|
pwsval |
|- ( ( R e. V /\ I e. W ) -> Y = ( F Xs_ ( I X. { R } ) ) ) |
12 |
7 8 11
|
syl2anc |
|- ( ph -> Y = ( F Xs_ ( I X. { R } ) ) ) |
13 |
12
|
fveq2d |
|- ( ph -> ( .s ` Y ) = ( .s ` ( F Xs_ ( I X. { R } ) ) ) ) |
14 |
4 13
|
eqtrid |
|- ( ph -> .xb = ( .s ` ( F Xs_ ( I X. { R } ) ) ) ) |
15 |
14
|
oveqd |
|- ( ph -> ( A .xb X ) = ( A ( .s ` ( F Xs_ ( I X. { R } ) ) ) X ) ) |
16 |
|
eqid |
|- ( F Xs_ ( I X. { R } ) ) = ( F Xs_ ( I X. { R } ) ) |
17 |
|
eqid |
|- ( Base ` ( F Xs_ ( I X. { R } ) ) ) = ( Base ` ( F Xs_ ( I X. { R } ) ) ) |
18 |
|
eqid |
|- ( .s ` ( F Xs_ ( I X. { R } ) ) ) = ( .s ` ( F Xs_ ( I X. { R } ) ) ) |
19 |
5
|
fvexi |
|- F e. _V |
20 |
19
|
a1i |
|- ( ph -> F e. _V ) |
21 |
|
fnconstg |
|- ( R e. V -> ( I X. { R } ) Fn I ) |
22 |
7 21
|
syl |
|- ( ph -> ( I X. { R } ) Fn I ) |
23 |
12
|
fveq2d |
|- ( ph -> ( Base ` Y ) = ( Base ` ( F Xs_ ( I X. { R } ) ) ) ) |
24 |
2 23
|
eqtrid |
|- ( ph -> B = ( Base ` ( F Xs_ ( I X. { R } ) ) ) ) |
25 |
10 24
|
eleqtrd |
|- ( ph -> X e. ( Base ` ( F Xs_ ( I X. { R } ) ) ) ) |
26 |
16 17 18 6 20 8 22 9 25
|
prdsvscaval |
|- ( ph -> ( A ( .s ` ( F Xs_ ( I X. { R } ) ) ) X ) = ( x e. I |-> ( A ( .s ` ( ( I X. { R } ) ` x ) ) ( X ` x ) ) ) ) |
27 |
|
fvconst2g |
|- ( ( R e. V /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R ) |
28 |
7 27
|
sylan |
|- ( ( ph /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R ) |
29 |
28
|
fveq2d |
|- ( ( ph /\ x e. I ) -> ( .s ` ( ( I X. { R } ) ` x ) ) = ( .s ` R ) ) |
30 |
29 3
|
eqtr4di |
|- ( ( ph /\ x e. I ) -> ( .s ` ( ( I X. { R } ) ` x ) ) = .x. ) |
31 |
30
|
oveqd |
|- ( ( ph /\ x e. I ) -> ( A ( .s ` ( ( I X. { R } ) ` x ) ) ( X ` x ) ) = ( A .x. ( X ` x ) ) ) |
32 |
31
|
mpteq2dva |
|- ( ph -> ( x e. I |-> ( A ( .s ` ( ( I X. { R } ) ` x ) ) ( X ` x ) ) ) = ( x e. I |-> ( A .x. ( X ` x ) ) ) ) |
33 |
9
|
adantr |
|- ( ( ph /\ x e. I ) -> A e. K ) |
34 |
|
fvexd |
|- ( ( ph /\ x e. I ) -> ( X ` x ) e. _V ) |
35 |
|
fconstmpt |
|- ( I X. { A } ) = ( x e. I |-> A ) |
36 |
35
|
a1i |
|- ( ph -> ( I X. { A } ) = ( x e. I |-> A ) ) |
37 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
38 |
1 37 2 7 8 10
|
pwselbas |
|- ( ph -> X : I --> ( Base ` R ) ) |
39 |
38
|
feqmptd |
|- ( ph -> X = ( x e. I |-> ( X ` x ) ) ) |
40 |
8 33 34 36 39
|
offval2 |
|- ( ph -> ( ( I X. { A } ) oF .x. X ) = ( x e. I |-> ( A .x. ( X ` x ) ) ) ) |
41 |
32 40
|
eqtr4d |
|- ( ph -> ( x e. I |-> ( A ( .s ` ( ( I X. { R } ) ` x ) ) ( X ` x ) ) ) = ( ( I X. { A } ) oF .x. X ) ) |
42 |
15 26 41
|
3eqtrd |
|- ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) ) |