Theorem rnascl

Description: The set of lifted 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		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		assalmod	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{LMod}$$
10		assaring	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{Ring}$$
11		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
12	11 2	ringidcl	$$⊢W\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_W$$
13	10 12	syl	$$⊢W\in \mathrm{AssAlg}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_W$$
14	4 5 11 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\}$$
15	9 13 14	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\}$$
16	8 15	eqtr4id	$$⊢W\in \mathrm{AssAlg}\to \mathrm{ran}A=N\left(\left\{\underset{\dot{}}{1}\right\}\right)$$