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 43065
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 43064 . 2 class LNoeM
2 vw . . . . . . 7 setvar 𝑤
32cv 1536 . . . . . 6 class 𝑤
4 vi . . . . . . 7 setvar 𝑖
54cv 1536 . . . . . 6 class 𝑖
6 cress 17274 . . . . . 6 class s
73, 5, 6co 7431 . . . . 5 class (𝑤s 𝑖)
8 clfig 43056 . . . . 5 class LFinGen
97, 8wcel 2106 . . . 4 wff (𝑤s 𝑖) ∈ LFinGen
10 clss 20947 . . . . 5 class LSubSp
113, 10cfv 6563 . . . 4 class (LSubSp‘𝑤)
129, 4, 11wral 3059 . . 3 wff 𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen
13 clmod 20875 . . 3 class LMod
1412, 2, 13crab 3433 . 2 class {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
151, 14wceq 1537 1 wff LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
Colors of variables: wff setvar class
This definition is referenced by:  islnm  43066
  Copyright terms: Public domain W3C validator