Step |
Hyp |
Ref |
Expression |
1 |
|
pwspjmhm.y |
|- Y = ( R ^s I ) |
2 |
|
pwspjmhm.b |
|- B = ( Base ` Y ) |
3 |
|
eqid |
|- ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) |
4 |
|
eqid |
|- ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) |
5 |
|
simp2 |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> I e. V ) |
6 |
|
fvexd |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( Scalar ` R ) e. _V ) |
7 |
|
fconst6g |
|- ( R e. Mnd -> ( I X. { R } ) : I --> Mnd ) |
8 |
7
|
3ad2ant1 |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( I X. { R } ) : I --> Mnd ) |
9 |
|
simp3 |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> A e. I ) |
10 |
3 4 5 6 8 9
|
prdspjmhm |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) |-> ( x ` A ) ) e. ( ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) MndHom ( ( I X. { R } ) ` A ) ) ) |
11 |
|
eqid |
|- ( Scalar ` R ) = ( Scalar ` R ) |
12 |
1 11
|
pwsval |
|- ( ( R e. Mnd /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) |
13 |
12
|
3adant3 |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) |
14 |
13
|
fveq2d |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( Base ` Y ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) |
15 |
2 14
|
syl5eq |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> B = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) |
16 |
15
|
mpteq1d |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. B |-> ( x ` A ) ) = ( x e. ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) |-> ( x ` A ) ) ) |
17 |
|
fvconst2g |
|- ( ( R e. Mnd /\ A e. I ) -> ( ( I X. { R } ) ` A ) = R ) |
18 |
17
|
3adant2 |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( ( I X. { R } ) ` A ) = R ) |
19 |
18
|
eqcomd |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> R = ( ( I X. { R } ) ` A ) ) |
20 |
13 19
|
oveq12d |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( Y MndHom R ) = ( ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) MndHom ( ( I X. { R } ) ` A ) ) ) |
21 |
10 16 20
|
3eltr4d |
|- ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) ) |