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 20729
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 20727 . 2 class LPIdeal
2 vw . . 3 setvar 𝑀
3 crg 19969 . . 3 class Ring
4 vg . . . 4 setvar 𝑔
52cv 1541 . . . . 5 class 𝑀
6 cbs 17088 . . . . 5 class Base
75, 6cfv 6497 . . . 4 class (Baseβ€˜π‘€)
84cv 1541 . . . . . . 7 class 𝑔
98csn 4587 . . . . . 6 class {𝑔}
10 crsp 20648 . . . . . . 7 class RSpan
115, 10cfv 6497 . . . . . 6 class (RSpanβ€˜π‘€)
129, 11cfv 6497 . . . . 5 class ((RSpanβ€˜π‘€)β€˜{𝑔})
1312csn 4587 . . . 4 class {((RSpanβ€˜π‘€)β€˜{𝑔})}
144, 7, 13ciun 4955 . . 3 class βˆͺ 𝑔 ∈ (Baseβ€˜π‘€){((RSpanβ€˜π‘€)β€˜{𝑔})}
152, 3, 14cmpt 5189 . 2 class (𝑀 ∈ Ring ↦ βˆͺ 𝑔 ∈ (Baseβ€˜π‘€){((RSpanβ€˜π‘€)β€˜{𝑔})})
161, 15wceq 1542 1 wff LPIdeal = (𝑀 ∈ Ring ↦ βˆͺ 𝑔 ∈ (Baseβ€˜π‘€){((RSpanβ€˜π‘€)β€˜{𝑔})})
Colors of variables: wff setvar class
This definition is referenced by:  lpival  20731
  Copyright terms: Public domain W3C validator