Definition df-rsp 21219

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

Assertion

Ref	Expression
df-rsp	⊢ RSpan = (LSpan ∘ ringLMod)

Detailed syntax breakdown of Definition df-rsp

Step	Hyp	Ref	Expression
1		crsp 21217	. 2 class RSpan
2		clspn 20969	. . 3 class LSpan
3		crglmod 21171	. . 3 class ringLMod
4	2, 3	ccom 5689	. 2 class (LSpan ∘ ringLMod)
5	1, 4	wceq 1540	1 wff RSpan = (LSpan ∘ ringLMod)

This definition is referenced by:  rspval  21221