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

Proof

Step	Hyp	Ref	Expression
1		rnascl.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		rnascl.o	⊢ 1 = ( 1r ‘ 𝑊 )
3		rnascl.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		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
10		assaring	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
11		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12	11 2	ringidcl	⊢ ( 𝑊 ∈ Ring → 1 ∈ ( Base ‘ 𝑊 ) )
13	10 12	syl	⊢ ( 𝑊 ∈ AssAlg → 1 ∈ ( Base ‘ 𝑊 ) )
14	4 5 11 6 3	lspsn	⊢ ( ( 𝑊 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ { 1 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) } )
15	9 13 14	syl2anc	⊢ ( 𝑊 ∈ AssAlg → ( 𝑁 ‘ { 1 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) } )
16	8 15	eqtr4id	⊢ ( 𝑊 ∈ AssAlg → ran 𝐴 = ( 𝑁 ‘ { 1 } ) )