Metamath Proof Explorer


Theorem rnascl

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 rnascl.a
|- A = ( algSc ` W )
rnascl.o
|- .1. = ( 1r ` W )
rnascl.n
|- N = ( LSpan ` W )
Assertion rnascl
|- ( W e. AssAlg -> ran A = ( N ` { .1. } ) )

Proof

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