Users' Mathboxes 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 38172
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 38171 . 2 class LNoeM
2 vw . . . . . . 7 setvar 𝑤
32cv 1630 . . . . . 6 class 𝑤
4 vi . . . . . . 7 setvar 𝑖
54cv 1630 . . . . . 6 class 𝑖
6 cress 16065 . . . . . 6 class s
73, 5, 6co 6793 . . . . 5 class (𝑤s 𝑖)
8 clfig 38163 . . . . 5 class LFinGen
97, 8wcel 2145 . . . 4 wff (𝑤s 𝑖) ∈ LFinGen
10 clss 19142 . . . . 5 class LSubSp
113, 10cfv 6031 . . . 4 class (LSubSp‘𝑤)
129, 4, 11wral 3061 . . 3 wff 𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen
13 clmod 19073 . . 3 class LMod
1412, 2, 13crab 3065 . 2 class {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
151, 14wceq 1631 1 wff LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
Colors of variables: wff setvar class
This definition is referenced by:  islnm  38173
  Copyright terms: Public domain W3C validator