Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lnm Structured version   Visualization version   GIF version

Definition df-lnm 40191
 Description: A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
Assertion
Ref Expression
df-lnm LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
Distinct variable group:   𝑤,𝑖

Detailed syntax breakdown of Definition df-lnm
StepHypRef Expression
1 clnm 40190 . 2 class LNoeM
2 vw . . . . . . 7 setvar 𝑤
32cv 1537 . . . . . 6 class 𝑤
4 vi . . . . . . 7 setvar 𝑖
54cv 1537 . . . . . 6 class 𝑖
6 cress 16496 . . . . . 6 class s
73, 5, 6co 7145 . . . . 5 class (𝑤s 𝑖)
8 clfig 40182 . . . . 5 class LFinGen
97, 8wcel 2111 . . . 4 wff (𝑤s 𝑖) ∈ LFinGen
10 clss 19717 . . . . 5 class LSubSp
113, 10cfv 6332 . . . 4 class (LSubSp‘𝑤)
129, 4, 11wral 3106 . . 3 wff 𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen
13 clmod 19648 . . 3 class LMod
1412, 2, 13crab 3110 . 2 class {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
151, 14wceq 1538 1 wff LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
 Colors of variables: wff setvar class This definition is referenced by:  islnm  40192
 Copyright terms: Public domain W3C validator