Definition df-rsp

Description: Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015)

	Ref	Expression
Assertion	df-rsp	$$⊢\mathrm{RSpan}=\mathrm{LSpan}\circ \mathrm{ringLMod}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crsp	$$class\mathrm{RSpan}$$
1		clspn	$$class\mathrm{LSpan}$$
2		crglmod	$$class\mathrm{ringLMod}$$
3	1 2	ccom	$$class\left(\mathrm{LSpan}\circ \mathrm{ringLMod}\right)$$
4	0 3	wceq	$$wff\mathrm{RSpan}=\mathrm{LSpan}\circ \mathrm{ringLMod}$$