df-rsp - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-rsp		Structured version Visualization version GIF version

Definition df-rsp 18996

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 18992	. 2 class RSpan
2		clspn 18792	. . 3 class LSpan
3		crglmod 18990	. . 3 class ringLMod
4	2, 3	ccom 5042	. 2 class (LSpan ∘ ringLMod)
5	1, 4	wceq 1475	1 wff RSpan = (LSpan ∘ ringLMod)

Colors of variables: wff setvar class

This definition is referenced by: rspval 19014