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	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	rnasclg.o	⊢ 1 = ( 1r ‘ 𝑊 )
	rnasclg.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	rnasclg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) → ran 𝐴 = ( 𝑁 ‘ { 1 } ) )

Proof

Step	Hyp	Ref	Expression
1		rnasclg.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		rnasclg.o	⊢ 1 = ( 1r ‘ 𝑊 )
3		rnasclg.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
6		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
7	1 4 5 6 2	asclfval	⊢ 𝐴 = ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↦ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) )
8	7	rnmpt	⊢ ran 𝐴 = { 𝑥 ∣ ∃ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) }
9		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10	9 2	ringidcl	⊢ ( 𝑊 ∈ Ring → 1 ∈ ( Base ‘ 𝑊 ) )
11	4 5 9 6 3	lspsn	⊢ ( ( 𝑊 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ { 1 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) } )
12	10 11	sylan2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) → ( 𝑁 ‘ { 1 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) } )
13	8 12	eqtr4id	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ) → ran 𝐴 = ( 𝑁 ‘ { 1 } ) )