Metamath Proof Explorer

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 o. ringLMod )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crsp 
 |-  RSpan
1 clspn 
 |-  LSpan
2 crglmod 
 |-  ringLMod
3 1 2 ccom 
 |-  ( LSpan o. ringLMod )
4 0 3 wceq 
 |-  RSpan = ( LSpan o. ringLMod )