Step |
Hyp |
Ref |
Expression |
1 |
|
rnascl.a |
|- A = ( algSc ` W ) |
2 |
|
rnascl.o |
|- .1. = ( 1r ` W ) |
3 |
|
rnascl.n |
|- N = ( LSpan ` W ) |
4 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
5 |
|
eqid |
|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
6 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
7 |
1 4 5 6 2
|
asclfval |
|- A = ( y e. ( Base ` ( Scalar ` W ) ) |-> ( y ( .s ` W ) .1. ) ) |
8 |
7
|
rnmpt |
|- ran A = { x | E. y e. ( Base ` ( Scalar ` W ) ) x = ( y ( .s ` W ) .1. ) } |
9 |
|
assalmod |
|- ( W e. AssAlg -> W e. LMod ) |
10 |
|
assaring |
|- ( W e. AssAlg -> W e. Ring ) |
11 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
12 |
11 2
|
ringidcl |
|- ( W e. Ring -> .1. e. ( Base ` W ) ) |
13 |
10 12
|
syl |
|- ( W e. AssAlg -> .1. e. ( Base ` W ) ) |
14 |
4 5 11 6 3
|
lspsn |
|- ( ( W e. LMod /\ .1. e. ( Base ` W ) ) -> ( N ` { .1. } ) = { x | E. y e. ( Base ` ( Scalar ` W ) ) x = ( y ( .s ` W ) .1. ) } ) |
15 |
9 13 14
|
syl2anc |
|- ( W e. AssAlg -> ( N ` { .1. } ) = { x | E. y e. ( Base ` ( Scalar ` W ) ) x = ( y ( .s ` W ) .1. ) } ) |
16 |
8 15
|
eqtr4id |
|- ( W e. AssAlg -> ran A = ( N ` { .1. } ) ) |