Metamath Proof Explorer


Theorem rnasclg

Description: The set of injected scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses rnasclg.a
|- A = ( algSc ` W )
rnasclg.o
|- .1. = ( 1r ` W )
rnasclg.n
|- N = ( LSpan ` W )
Assertion rnasclg
|- ( ( W e. LMod /\ W e. Ring ) -> ran A = ( N ` { .1. } ) )

Proof

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. } ) )