| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psrasclcl.s |
|- S = ( I mPwSer R ) |
| 2 |
|
psrasclcl.b |
|- B = ( Base ` S ) |
| 3 |
|
psrasclcl.k |
|- K = ( Base ` R ) |
| 4 |
|
psrasclcl.a |
|- A = ( algSc ` S ) |
| 5 |
|
psrasclcl.i |
|- ( ph -> I e. W ) |
| 6 |
|
psrasclcl.r |
|- ( ph -> R e. Ring ) |
| 7 |
|
psrasclcl.c |
|- ( ph -> C e. K ) |
| 8 |
|
eqid |
|- ( Scalar ` S ) = ( Scalar ` S ) |
| 9 |
1 5 6
|
psrring |
|- ( ph -> S e. Ring ) |
| 10 |
1 5 6
|
psrlmod |
|- ( ph -> S e. LMod ) |
| 11 |
|
eqid |
|- ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) ) |
| 12 |
4 8 9 10 11 2
|
asclf |
|- ( ph -> A : ( Base ` ( Scalar ` S ) ) --> B ) |
| 13 |
1 5 6
|
psrsca |
|- ( ph -> R = ( Scalar ` S ) ) |
| 14 |
13
|
fveq2d |
|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` S ) ) ) |
| 15 |
3 14
|
eqtrid |
|- ( ph -> K = ( Base ` ( Scalar ` S ) ) ) |
| 16 |
15
|
feq2d |
|- ( ph -> ( A : K --> B <-> A : ( Base ` ( Scalar ` S ) ) --> B ) ) |
| 17 |
12 16
|
mpbird |
|- ( ph -> A : K --> B ) |
| 18 |
17 7
|
ffvelcdmd |
|- ( ph -> ( A ` C ) e. B ) |