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=\mathrm{algSc}\left(W\right)$$
	rnascl.o	$$⊢\underset{\dot{}}{1}=1_W$$
	rnascl.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	rnascl	$$⊢W\in \mathrm{AssAlg}\to \mathrm{ran}A=N\left(\left\{\underset{\dot{}}{1}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rnascl.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		rnascl.o	$$⊢\underset{\dot{}}{1}=1_W$$
3		rnascl.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		assalmod	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{LMod}$$
5		assaring	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{Ring}$$
6		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
7	6 2	ringidcl	$$⊢W\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_W$$
8	5 7	syl	$$⊢W\in \mathrm{AssAlg}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_W$$
9		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
11		eqid	$$⊢{\cdot }_W={\cdot }_W$$
12	9 10 6 11 3	lspsn	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_W\right)\to N\left(\left\{\underset{\dot{}}{1}\right\}\right)=\left\{x|\exists y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=y{\cdot }_W\underset{\dot{}}{1}\right\}$$
13	4 8 12	syl2anc	$$⊢W\in \mathrm{AssAlg}\to N\left(\left\{\underset{\dot{}}{1}\right\}\right)=\left\{x|\exists y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=y{\cdot }_W\underset{\dot{}}{1}\right\}$$
14	1 9 10 11 2	asclfval	$$⊢A=\left(y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟼y{\cdot }_W\underset{\dot{}}{1}\right)$$
15	14	rnmpt	$$⊢\mathrm{ran}A=\left\{x|\exists y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=y{\cdot }_W\underset{\dot{}}{1}\right\}$$
16	13 15	syl6reqr	$$⊢W\in \mathrm{AssAlg}\to \mathrm{ran}A=N\left(\left\{\underset{\dot{}}{1}\right\}\right)$$