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

Definition df-lpidl 21081
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 = (𝑀 ∈ Ring ↦ βˆͺ 𝑔 ∈ (Baseβ€˜π‘€){((RSpanβ€˜π‘€)β€˜{𝑔})})
Distinct variable group:   𝑀,𝑔

Detailed syntax breakdown of Definition df-lpidl
StepHypRef Expression
1 clpidl 21079 . 2 class LPIdeal
2 vw . . 3 setvar 𝑀
3 crg 20127 . . 3 class Ring
4 vg . . . 4 setvar 𝑔
52cv 1538 . . . . 5 class 𝑀
6 cbs 17148 . . . . 5 class Base
75, 6cfv 6542 . . . 4 class (Baseβ€˜π‘€)
84cv 1538 . . . . . . 7 class 𝑔
98csn 4627 . . . . . 6 class {𝑔}
10 crsp 20929 . . . . . . 7 class RSpan
115, 10cfv 6542 . . . . . 6 class (RSpanβ€˜π‘€)
129, 11cfv 6542 . . . . 5 class ((RSpanβ€˜π‘€)β€˜{𝑔})
1312csn 4627 . . . 4 class {((RSpanβ€˜π‘€)β€˜{𝑔})}
144, 7, 13ciun 4996 . . 3 class βˆͺ 𝑔 ∈ (Baseβ€˜π‘€){((RSpanβ€˜π‘€)β€˜{𝑔})}
152, 3, 14cmpt 5230 . 2 class (𝑀 ∈ Ring ↦ βˆͺ 𝑔 ∈ (Baseβ€˜π‘€){((RSpanβ€˜π‘€)β€˜{𝑔})})
161, 15wceq 1539 1 wff LPIdeal = (𝑀 ∈ Ring ↦ βˆͺ 𝑔 ∈ (Baseβ€˜π‘€){((RSpanβ€˜π‘€)β€˜{𝑔})})
Colors of variables: wff setvar class
This definition is referenced by:  lpival  21083
  Copyright terms: Public domain W3C validator