| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ressasclcl.w |
|- W = ( Poly1 ` U ) |
| 2 |
|
ressasclcl.u |
|- U = ( S |`s R ) |
| 3 |
|
ressasclcl.a |
|- A = ( algSc ` W ) |
| 4 |
|
ressasclcl.1 |
|- B = ( Base ` W ) |
| 5 |
|
ressasclcl.s |
|- ( ph -> S e. CRing ) |
| 6 |
|
ressasclcl.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 7 |
|
ressasclcl.x |
|- ( ph -> X e. R ) |
| 8 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
| 9 |
8
|
subrgss |
|- ( R e. ( SubRing ` S ) -> R C_ ( Base ` S ) ) |
| 10 |
2 8
|
ressbas2 |
|- ( R C_ ( Base ` S ) -> R = ( Base ` U ) ) |
| 11 |
6 9 10
|
3syl |
|- ( ph -> R = ( Base ` U ) ) |
| 12 |
2
|
subrgcrng |
|- ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> U e. CRing ) |
| 13 |
5 6 12
|
syl2anc |
|- ( ph -> U e. CRing ) |
| 14 |
1
|
ply1sca |
|- ( U e. CRing -> U = ( Scalar ` W ) ) |
| 15 |
13 14
|
syl |
|- ( ph -> U = ( Scalar ` W ) ) |
| 16 |
15
|
fveq2d |
|- ( ph -> ( Base ` U ) = ( Base ` ( Scalar ` W ) ) ) |
| 17 |
11 16
|
eqtrd |
|- ( ph -> R = ( Base ` ( Scalar ` W ) ) ) |
| 18 |
7 17
|
eleqtrd |
|- ( ph -> X e. ( Base ` ( Scalar ` W ) ) ) |
| 19 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
| 20 |
|
eqid |
|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
| 21 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
| 22 |
|
eqid |
|- ( 1r ` W ) = ( 1r ` W ) |
| 23 |
3 19 20 21 22
|
asclval |
|- ( X e. ( Base ` ( Scalar ` W ) ) -> ( A ` X ) = ( X ( .s ` W ) ( 1r ` W ) ) ) |
| 24 |
18 23
|
syl |
|- ( ph -> ( A ` X ) = ( X ( .s ` W ) ( 1r ` W ) ) ) |
| 25 |
13
|
crngringd |
|- ( ph -> U e. Ring ) |
| 26 |
1
|
ply1lmod |
|- ( U e. Ring -> W e. LMod ) |
| 27 |
25 26
|
syl |
|- ( ph -> W e. LMod ) |
| 28 |
1
|
ply1ring |
|- ( U e. Ring -> W e. Ring ) |
| 29 |
4 22
|
ringidcl |
|- ( W e. Ring -> ( 1r ` W ) e. B ) |
| 30 |
25 28 29
|
3syl |
|- ( ph -> ( 1r ` W ) e. B ) |
| 31 |
4 19 21 20 27 18 30
|
lmodvscld |
|- ( ph -> ( X ( .s ` W ) ( 1r ` W ) ) e. B ) |
| 32 |
24 31
|
eqeltrd |
|- ( ph -> ( A ` X ) e. B ) |