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

Proof

Step	Hyp	Ref	Expression
1		rnasclg.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		rnasclg.o	$$⊢\underset{\dot{}}{1}=1_W$$
3		rnasclg.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
5	4 2	ringidcl	$$⊢W\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_W$$
6		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
7		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
8		eqid	$$⊢{\cdot }_W={\cdot }_W$$
9	6 7 4 8 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\}$$
10	5 9	sylan2	$$⊢\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\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\}$$
11	1 6 7 8 2	asclfval	$$⊢A=\left(y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟼y{\cdot }_W\underset{\dot{}}{1}\right)$$
12	11	rnmpt	$$⊢\mathrm{ran}A=\left\{x|\exists y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=y{\cdot }_W\underset{\dot{}}{1}\right\}$$
13	10 12	syl6reqr	$$⊢\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\right)\to \mathrm{ran}A=N\left(\left\{\underset{\dot{}}{1}\right\}\right)$$