MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lpidl Unicode version

Definition df-lpidl 15995
Description: Define the class of left principal ideals of a ring, which are ideals with a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
Assertion
Ref Expression
df-lpidl  |- LPIdeal  =  ( w  e.  Ring  |->  U_ g  e.  ( Base `  w
) { ( (RSpan `  w ) `  {
g } ) } )
Distinct variable group:    w, g

Detailed syntax breakdown of Definition df-lpidl
StepHypRef Expression
1 clpidl 15993 . 2  class LPIdeal
2 vw . . 3  set  w
3 crg 15337 . . 3  class  Ring
4 vg . . . 4  set  g
52cv 1622 . . . . 5  class  w
6 cbs 13148 . . . . 5  class  Base
75, 6cfv 5255 . . . 4  class  ( Base `  w )
84cv 1622 . . . . . . 7  class  g
98csn 3640 . . . . . 6  class  { g }
10 crsp 15924 . . . . . . 7  class RSpan
115, 10cfv 5255 . . . . . 6  class  (RSpan `  w )
129, 11cfv 5255 . . . . 5  class  ( (RSpan `  w ) `  {
g } )
1312csn 3640 . . . 4  class  { ( (RSpan `  w ) `  { g } ) }
144, 7, 13ciun 3905 . . 3  class  U_ g  e.  ( Base `  w
) { ( (RSpan `  w ) `  {
g } ) }
152, 3, 14cmpt 4077 . 2  class  ( w  e.  Ring  |->  U_ g  e.  ( Base `  w
) { ( (RSpan `  w ) `  {
g } ) } )
161, 15wceq 1623 1  wff LPIdeal  =  ( w  e.  Ring  |->  U_ g  e.  ( Base `  w
) { ( (RSpan `  w ) `  {
g } ) } )
Colors of variables: wff set class
This definition is referenced by:  lpival  15997
  Copyright terms: Public domain W3C validator