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

Definition df-lpidl 19224
 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 19222 . 2 class LPIdeal
2 vw . . 3 setvar 𝑤
3 crg 18528 . . 3 class Ring
4 vg . . . 4 setvar 𝑔
52cv 1480 . . . . 5 class 𝑤
6 cbs 15838 . . . . 5 class Base
75, 6cfv 5876 . . . 4 class (Base‘𝑤)
84cv 1480 . . . . . . 7 class 𝑔
98csn 4168 . . . . . 6 class {𝑔}
10 crsp 19152 . . . . . . 7 class RSpan
115, 10cfv 5876 . . . . . 6 class (RSpan‘𝑤)
129, 11cfv 5876 . . . . 5 class ((RSpan‘𝑤)‘{𝑔})
1312csn 4168 . . . 4 class {((RSpan‘𝑤)‘{𝑔})}
144, 7, 13ciun 4511 . . 3 class 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})}
152, 3, 14cmpt 4720 . 2 class (𝑤 ∈ Ring ↦ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})
161, 15wceq 1481 1 wff LPIdeal = (𝑤 ∈ Ring ↦ 𝑔 ∈ (Base‘𝑤){((RSpan‘𝑤)‘{𝑔})})
 Colors of variables: wff setvar class This definition is referenced by:  lpival  19226
 Copyright terms: Public domain W3C validator