Step |
Hyp |
Ref |
Expression |
1 |
|
rnasclg.a |
|- A = ( algSc ` W ) |
2 |
|
rnasclg.o |
|- .1. = ( 1r ` W ) |
3 |
|
rnasclg.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 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
10 |
9 2
|
ringidcl |
|- ( W e. Ring -> .1. e. ( Base ` W ) ) |
11 |
4 5 9 6 3
|
lspsn |
|- ( ( W e. LMod /\ .1. e. ( Base ` W ) ) -> ( N ` { .1. } ) = { x | E. y e. ( Base ` ( Scalar ` W ) ) x = ( y ( .s ` W ) .1. ) } ) |
12 |
10 11
|
sylan2 |
|- ( ( W e. LMod /\ W e. Ring ) -> ( N ` { .1. } ) = { x | E. y e. ( Base ` ( Scalar ` W ) ) x = ( y ( .s ` W ) .1. ) } ) |
13 |
8 12
|
eqtr4id |
|- ( ( W e. LMod /\ W e. Ring ) -> ran A = ( N ` { .1. } ) ) |