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

Definition df-lpidl 17433
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 17431 . 2  class LPIdeal
2 vw . . 3  setvar  w
3 crg 16753 . . 3  class  Ring
4 vg . . . 4  setvar  g
52cv 1369 . . . . 5  class  w
6 cbs 14278 . . . . 5  class  Base
75, 6cfv 5518 . . . 4  class  ( Base `  w )
84cv 1369 . . . . . . 7  class  g
98csn 3977 . . . . . 6  class  { g }
10 crsp 17360 . . . . . . 7  class RSpan
115, 10cfv 5518 . . . . . 6  class  (RSpan `  w )
129, 11cfv 5518 . . . . 5  class  ( (RSpan `  w ) `  {
g } )
1312csn 3977 . . . 4  class  { ( (RSpan `  w ) `  { g } ) }
144, 7, 13ciun 4271 . . 3  class  U_ g  e.  ( Base `  w
) { ( (RSpan `  w ) `  {
g } ) }
152, 3, 14cmpt 4450 . 2  class  ( w  e.  Ring  |->  U_ g  e.  ( Base `  w
) { ( (RSpan `  w ) `  {
g } ) } )
161, 15wceq 1370 1  wff LPIdeal  =  ( w  e.  Ring  |->  U_ g  e.  ( Base `  w
) { ( (RSpan `  w ) `  {
g } ) } )
Colors of variables: wff setvar class
This definition is referenced by:  lpival  17435
  Copyright terms: Public domain W3C validator