Step |
Hyp |
Ref |
Expression |
1 |
|
ascl0.a |
|- A = ( algSc ` W ) |
2 |
|
ascl0.f |
|- F = ( Scalar ` W ) |
3 |
|
ascl0.l |
|- ( ph -> W e. LMod ) |
4 |
|
ascl0.r |
|- ( ph -> W e. Ring ) |
5 |
2
|
lmodring |
|- ( W e. LMod -> F e. Ring ) |
6 |
|
eqid |
|- ( Base ` F ) = ( Base ` F ) |
7 |
|
eqid |
|- ( 1r ` F ) = ( 1r ` F ) |
8 |
6 7
|
ringidcl |
|- ( F e. Ring -> ( 1r ` F ) e. ( Base ` F ) ) |
9 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
10 |
|
eqid |
|- ( 1r ` W ) = ( 1r ` W ) |
11 |
1 2 6 9 10
|
asclval |
|- ( ( 1r ` F ) e. ( Base ` F ) -> ( A ` ( 1r ` F ) ) = ( ( 1r ` F ) ( .s ` W ) ( 1r ` W ) ) ) |
12 |
3 5 8 11
|
4syl |
|- ( ph -> ( A ` ( 1r ` F ) ) = ( ( 1r ` F ) ( .s ` W ) ( 1r ` W ) ) ) |
13 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
14 |
13 10
|
ringidcl |
|- ( W e. Ring -> ( 1r ` W ) e. ( Base ` W ) ) |
15 |
4 14
|
syl |
|- ( ph -> ( 1r ` W ) e. ( Base ` W ) ) |
16 |
13 2 9 7
|
lmodvs1 |
|- ( ( W e. LMod /\ ( 1r ` W ) e. ( Base ` W ) ) -> ( ( 1r ` F ) ( .s ` W ) ( 1r ` W ) ) = ( 1r ` W ) ) |
17 |
3 15 16
|
syl2anc |
|- ( ph -> ( ( 1r ` F ) ( .s ` W ) ( 1r ` W ) ) = ( 1r ` W ) ) |
18 |
12 17
|
eqtrd |
|- ( ph -> ( A ` ( 1r ` F ) ) = ( 1r ` W ) ) |