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