Theorem rspcl

Description: The span of a set of ring elements is an ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)

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

Proof

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