Theorem rspssid

Description: The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	rspcl.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	rspcl.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	rspssid	$$⊢\left(R\in \mathrm{Ring}\wedge G\subseteq B\right)\to G\subseteq K\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		rspcl.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
2		rspcl.b	$$⊢B={\mathrm{Base}}_R$$
3		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
4		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
5	2 4	eqtri	$$⊢B={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
6		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
7	1 6	eqtri	$$⊢K=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
8	5 7	lspssid	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\wedge G\subseteq B\right)\to G\subseteq K\left(G\right)$$
9	3 8	sylan	$$⊢\left(R\in \mathrm{Ring}\wedge G\subseteq B\right)\to G\subseteq K\left(G\right)$$