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	⊢ RSpan = ( LSpan ∘ ringLMod )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crsp	⊢ RSpan
1		clspn	⊢ LSpan
2		crglmod	⊢ ringLMod
3	1 2	ccom	⊢ ( LSpan ∘ ringLMod )
4	0 3	wceq	⊢ RSpan = ( LSpan ∘ ringLMod )