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 19006
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 19004 . 2 class LPIdeal
2 vw . . 3 setvar 𝑤
3 crg 18312 . . 3 class Ring
4 vg . . . 4 setvar 𝑔
52cv 1473 . . . . 5 class 𝑤
6 cbs 15637 . . . . 5 class Base
75, 6cfv 5786 . . . 4 class (Base‘𝑤)
84cv 1473 . . . . . . 7 class 𝑔
98csn 4120 . . . . . 6 class {𝑔}
10 crsp 18934 . . . . . . 7 class RSpan
115, 10cfv 5786 . . . . . 6 class (RSpan‘𝑤)
129, 11cfv 5786 . . . . 5 class ((RSpan‘𝑤)‘{𝑔})
1312csn 4120 . . . 4 class {((RSpan‘𝑤)‘{𝑔})}
144, 7, 13ciun 4445 . . 3 class 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})}
152, 3, 14cmpt 4633 . 2 class (𝑤 ∈ Ring ↦ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})
161, 15wceq 1474 1 wff LPIdeal = (𝑤 ∈ Ring ↦ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})
Colors of variables: wff setvar class
This definition is referenced by:  lpival  19008
  Copyright terms: Public domain W3C validator