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