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{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
5		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
6		eqid	$$⊢{\cdot }_W={\cdot }_W$$
7	1 4 5 6 2	asclfval	$$⊢A=\left(y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟼y{\cdot }_W\underset{\dot{}}{1}\right)$$
8	7	rnmpt	$$⊢\mathrm{ran}A=\left\{x|\exists y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}x=y{\cdot }_W\underset{\dot{}}{1}\right\}$$
9		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
10	9 2	ringidcl	$$⊢W\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_W$$
11	4 5 9 6 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\}$$
12	10 11	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\}$$
13	8 12	eqtr4id	$$⊢\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\right)\to \mathrm{ran}A=N\left(\left\{\underset{\dot{}}{1}\right\}\right)$$